Create a gist now

Instantly share code, notes, and snippets.

@echojc /λ-calculus.scala Secret
Last active Sep 27, 2015

What would you like to do?
import scala.language.higherKinds
object Main {
// allows "printing" the type in the repl
def show[T]: T = null.asInstanceOf[T]
// base type to say that "all things can apply"
trait λ { type Ap[X <: λ] <: λ }
// SKI combinators
trait S extends λ { trait Ap[X <: λ]
extends λ { trait Ap[Y <: λ]
extends λ { type Ap[Z <: λ] = X#Ap[Z]#Ap[Y#Ap[Z]] }}}
trait K extends λ { trait Ap[X <: λ]
extends λ { type Ap[Y <: λ] = X }}
type I = S#Ap[K]#Ap[K]
// function operations
type Ap = S#Ap[S#Ap[K]]
type Comp = S#Ap[K#Ap[S]]#Ap[K]
type Flip = S#Ap[K#Ap[S#Ap[I]]]#Ap[K]
// boolean logic
type True = K
type False = S#Ap[K]
type And = S#Ap[S]#Ap[K#Ap[K#Ap[False]]]
type Or = S#Ap[I]#Ap[K#Ap[True]]
type Not = S#Ap[K#Ap[Flip#Ap[True]]]#Ap[Flip#Ap[False]]
// numbers
type _0 = False
type Succ = S#Ap[Comp]
type _1 = Succ#Ap[_0]
type _2 = Succ#Ap[_1]
type _3 = Succ#Ap[_2]
type _4 = Succ#Ap[_3]
type _5 = Succ#Ap[_4]
type _6 = Succ#Ap[_5]
type IsZero = S#Ap[K#Ap[Flip#Ap[True]]]#Ap[Flip#Ap[K#Ap[False]]]
type Add = S#Ap[I]#Ap[K#Ap[Succ]]
// scala can't reconcile this definition with Succ^n#Ap[_0] - why not? it works out on paper
//type Mul = Comp
trait Mul extends λ { trait Ap[X <: λ]
extends λ { type Ap[Y <: λ] = X#Ap[Y#Ap[Succ]]#Ap[_0] }}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment