Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
object DeBruijn {
sealed trait Nat
sealed trait Z extends Nat
sealed trait S[n <: Nat] extends Nat
sealed trait Fin[n <: Nat]
case class FZ[n <: Nat]() extends Fin[S[n]]
case class FS[n <: Nat](n : Fin[n]) extends Fin[S[n]]
val here : Fin[S[S[Z]]] = FZ()
val there : Fin[S[S[Z]]] = FS(FZ())
// val invalid : Var[S[S[Z]]] = VS(VS(VZ()))
sealed trait Term[n <: Nat]
case class Var[n <: Nat](x : Fin[n]) extends Term[n]
case class Lambda[n <: Nat](t : Term[S[n]]) extends Term[n]
case class App[n <: Nat](f : Term[n], t : Term[n]) extends Term[n]
// `(\x.x) y` where `y` is the only free variable
val example : Term[S[Z]] = App(Lambda(Var(FZ())), Var(FZ()))
def thin[n <: Nat] : Fin[S[n]] => Fin[n] => Fin[S[n]] = {
case FZ() => y => FS(y)
case FS(n) => {
case FZ() => FZ()
case FS(m) => FS(thin(n)(m))
}
}
def rename[n <: Nat, m <: Nat] : (Fin[n] => Fin[m]) => (Fin[n] => Term[m]) =
f => i => Var(f(i))
def lift[n <: Nat, m <: Nat] : (Fin[n] => Term[m]) => (Fin[S[n]] => Term[S[m]]) = f => {
case FZ() => Var(FZ())
case FS(x) => subst (rename ((y : Fin[m]) => FS(y))) (f(x))
}
def subst[n <: Nat, m <: Nat] : (Fin[n] => Term[m]) => (Term[n] => Term[m]) = f => {
case Var(x) => f(x)
case Lambda(t) => Lambda(subst(lift(f))(t))
case App(t, e) => App(subst(f)(t), subst(f)(e))
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment