λ-calculus.scala

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] }}
}