Type level lambda calculus in Scala
This repository demonstrates an implementation of lambda calculus in Scala types.
import lambda._
case class Equals[A >: B <: B, B]() // this checks type equality
type S = x ->: y ->: z ->: ( x @@ z @@ (y @@ z) )
type K = x ->: y ->: x
type result = ( S @@ K @@ K @@ a ) # ->*
Equals[result, a]
More examples are found in TermSpec.scala.
Code | |
---|---|
Variables |
a , b , ..., z
|
Abstraction | v ->: M |
Application | M @@ N |
Terms |
M , N
|
1-step beta reduction | M # -> |
Multi-step beta reduction | M # ->* |
You can define your own variables by calling #next
of existing (last defined) variable
type variableName1 = z #next
type variableName2 = variableName1 #next
You may need parenthesis to avoid ambiguity
Lambda terms are converted internally to De Bruijn indexed terms and indices are shifted during substitution to ensure capture-avoiding semantics.