KO | EN

GitLite

Minimalist Open Source Repository Search Engine

gitlite — search

#developer-tools #typescript #codex #ai-agents #claude-code #dsh #dsh-plugin #cli #macos #ai-agent #deepseek-harness #open-source

scala-bound

★ 28 Open GitHub ↗

A library for developing languages with scoped binders (like forall or lambda).

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

Bound
=====

A library for developing languages with scoped binders (like forall or lambda).

This is a Scala port of [Edward Kmett's Bound library for Haskell](https://github.com/ekmett/bound).

Getting started
---------------

###Add this your build.sbt file:###

```
resolvers += "Runar's Bintray Repo" at "http://dl.bintray.com/runarorama/maven/"

libraryDependencies += "bound" %% "bound-core" % "1.3.0"
```

Binary packages available at https://bintray.com/runarorama/maven/bound

This library provides convenient combinators for working with "locally-nameless" terms. These can be useful when writing a type checker, evaluator, parser, or pretty-printer for terms that contain binders like forall or lambda. They ease the task of avoiding variable capture and testing for alpha-equivalence.

Example
-------

```scala
import scalaz._
import scalaz.std.string._
import bound._

// An untyped lambda calculus
sealed trait Exp[+A] {
  def apply[B >: A](arg: Exp[B]): Exp[B] = App(this, arg)
}
case class V[+A](a: A) extends Exp[A]
case class App[+A](fn: Exp[A], arg: Exp[A]) extends Exp[A]
case class Lam[+A](s: Scope[Unit, Exp, A]) extends Exp[A]

// A monad for our calculus
implicit val expMonad: Monad[Exp] = new Monad[Exp] {
  def point[A](a: => A) = V(a)
  def bind[A,B](m: Exp[A])(f: A => Exp[B]): Exp[B] = m match {
    case V(a)   => f(a)
    case App(x,y) => App(bind(x)(f), bind(y)(f))
    case Lam(e)   => Lam(e >>>= f)
  }
}

// Lambda abstraction smart constructor.
def lam[A:Equal](v: A, b: Exp[A]): Exp[A] =
  Lam(abstract1(v, b))

// Weak-head normal form evaluator.
def whnf[A](e: Exp[A]): Exp[A] = e match {
  case App(f,a) => whnf(f) match {
    case Lam(b) => whnf(instantiate1(a,b))
    case g      => App(g,a)
  }
  case e => e
}
```

We can then construct and evaluate lambda terms in the console. The `const` function contains two nested scopes. Note that the variable names are erased. What remains are two nested scopes.
The `-\/` indicates a term bound in the outer scope. The `\/-` indicates a free term.

scala> val const = lam("x", lam("y", V("x")))
    const: Exp[String] = Lam(Scope(Lam(Scope(V(\/-(V(-\/(()))))))))
    
The part that is the outer scope is `Lam(Scope(...V(-\/(()))...))`. The inner scope is `...Lam(Scope(V(\/-(...))))...`. So what used to be `x` is bound in the outer scope and free in the inner scope.
    
Applying this term to the named variable `V("a")` we are left with a lambda term whose free term has been instantiated to `V("a")`.

scala> val constA = whnf(const(V("a")))
    p: Exp[String] = Lam(Scope(V(\/-(V(a)))))

Applying that to a second term gives us the term we bound to the variable:

scala> val a = whnf(constA(V("b")))
    a: Exp[String] = V(a)

scala-bound

Explore Similar Repositories

Was this content helpful?

Recent Feedback

Download README