Encoding the lambda calculus and SKI calculus in Scala's type system.

LambdaCalculus.scala

import scala.language.higherKinds

// https://apocalisp.wordpress.com/2009/09/02/more-scala-typehackery/

// http://scala-lang.org/blog/2016/02/17/scaling-dot-soundness.html
// There is a proposed fix to disallow this, but there may be other ways to
// get Turing-completeness.

trait Lambda {
  type subst[U <: Lambda] <: Lambda
  type apply[U <: Lambda] <: Lambda
  type eval <: Lambda
}

trait App[S <: Lambda, T <: Lambda] extends Lambda {
  type subst[U <: Lambda] = App[S#subst[U], T#subst[U]]
  type apply[U] = Nothing
  type eval = S#eval#apply[T]
}

trait Lam[T <: Lambda] extends Lambda {
  type subst[U <: Lambda] = Lam[T]
  type apply[U <: Lambda] = T#subst[U]#eval
  type eval = Lam[T]
}

trait X extends Lambda {
  type subst[U <: Lambda] = U
  type apply[U] = Lambda
  type eval = X
}

trait Equal[T1 >: T2 <: T2, T2]

object Main {
  type T1 = Equal[App[Lam[X], X]#eval, X] // OK
//  type T2 = Equal[App[Lam[X], X]#eval, Lam[X]] // won't compmile

  // evaluates (λx.xx)(λx.xx) which is an infinite loop
//  type T3 = App[Lam[App[X, X]], Lam[App[X, X]]]#eval // stack overflow
}

SKI.scala

import scala.language.higherKinds

// https://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/

// http://scala-lang.org/blog/2016/02/17/scaling-dot-soundness.html
// There is a proposed fix to disallow this, but there may be other ways to
// get Turing-completeness.

trait Term {
  type ap[x <: Term] <: Term
  type eval <: Term
}

// The S combinator
trait S extends Term {
  type ap[x <: Term] = S1[x]
  type eval = S
}
trait S1[x <: Term] extends Term {
  type ap[y <: Term] = S2[x, y]
  type eval = S1[x]
}
trait S2[x <: Term, y <: Term] extends Term {
  type ap[z <: Term] = S3[x, y, z]
  type eval = S2[x, y]
}
trait S3[x <: Term, y <: Term, z <: Term] extends Term {
  type ap[v <: Term] = eval#ap[v]
  type eval = x#ap[z]#ap[y#ap[z]]#eval
}

// The K combinator
trait K extends Term {
  type ap[x <: Term] = K1[x]
  type eval = K
}
trait K1[x <: Term] extends Term {
  type ap[y <: Term] = K2[x, y]
  type eval = K1[x]
}
trait K2[x <: Term, y <: Term] extends Term {
  type ap[z <: Term] = eval#ap[z]
  type eval = x#eval
}

// The I combinator
trait I extends Term {
  type ap[x <: Term] = I1[x]
  type eval = I
}
trait I1[x <: Term] extends Term {
  type ap[y <: Term] = eval#ap[y]
  type eval = x#eval
}
trait c extends Term {
  type ap[x <: Term] = c
  type eval = c
}
trait d extends Term {
  type ap[x <: Term] = d
  type eval = d
}
trait e extends Term {
  type ap[x <: Term] = e
  type eval = e
}

case class Equals[A >: B <:B , B]()

object Main{
  // R = S(K(SI))K  (reverse)
  type R = S#ap[K#ap[S#ap[I]]]#ap[K]

  // β(a) = S(Ka)(SII)
  type b[a <: Term] = S#ap[K#ap[a]]#ap[S#ap[I]#ap[I]]

  trait An extends Term {
    type ap[x <: Term] = x#ap[An]#eval
    type eval = An
  }

  // Ic -> c
  type T1 = Equals[I#ap[c]#eval, c] // OK
//  type T2 = Equals[I#ap[c]#eval, d] // won't compile

  // Infinite iteration: Smashes scalac's stack
  type NNn = b[R]#ap[b[R]]#ap[An]
//  type T3 = Equals[NNn#eval, c]
}