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.

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

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)