ChurchNat.scala

object Main {
  def imp[T](implicit t: T): t.type {} = t

  trait Value[T] {
    type Type
    def value: Type
  }
  object Value {
    type Aux[T, V] = Value[T] { type Type = V }

    def aux[T, V](v: V): Value.Aux[T, V] =
      new Value[T] { type Type = V; val value = v }
  }

  type Nat
  object Nat {
    type Z <: Nat
    type S[N <: Nat] <: Nat

    implicit val zValue: Value.Aux[Z, Int] =
      Value.aux[Z, Int](0)
    implicit def sValue[N <: Nat]
    (implicit N: Value.Aux[N, Int]): Value.Aux[S[N], Int] =
      Value.aux[S[N], Int](N.value + 1)
  }

  object Church {
    object Nat {
      type Z
        = [K, z <: K, s[_ <: K] <: K] => z
      type S[N[K, _ <: K, _[_ <: K] <: K] <: K]
        = [K, z <: K, s[_ <: K] <: K] => s[N[K, z, s]]
      type +[M[K, _ <: K, _[_ <: K] <: K] <: K,
             N[K, _ <: K, _[_ <: K] <: K] <: K]
        = [K, z <: K, s[_ <: K] <: K] => M[K, N[K, z, s], [T <: K] => s[T]]

      type Cata[N[K, _ <: K, _[_ <: K] <: K] <: K, K, z <: K, s[_ <: K] <: K] =
        N[K, z, s]
    }
  }

  def main(args: Array[String]): Unit = {
    import Church.Nat._
    type N = S[S[Z]] + S[Z]

    {
      import Nat._
      type X = Church.Nat.Cata[N, Nat, Z, S]
      imp[X =:= S[S[S[Z]]]]
      println(imp[Value[X]].value)
    }
  }
}