Skip to content

Instantly share code, notes, and snippets.

@umazalakain
Last active May 10, 2022 09:45
Show Gist options
  • Star 2 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save umazalakain/a866e42683e0f0e220fed67668404505 to your computer and use it in GitHub Desktop.
Save umazalakain/a866e42683e0f0e220fed67668404505 to your computer and use it in GitHub Desktop.
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