Last active
May 10, 2022 09:45
-
-
Save umazalakain/a866e42683e0f0e220fed67668404505 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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