Simple example of type-level church encoding

TLChurch.scala

object tl_church {

  trait Booleans {
    type Bool <: { type Not <: Bool }
    type True <: Bool
    type False <: Bool
  }

  trait Nats {
    type Nat
    type Zero <: Nat
    type Succ[N <: Nat] <: Nat
  }


  // Example Client
  
  trait Client {
    val nats: Nats; import nats._

    val x: Succ[Succ[Succ[Zero]]] = ???
    val y: Succ[Succ[Zero]] = ???
  }


  // Some Implementations

  trait IsEven extends Nats {
    val booleans: Booleans; import booleans._
    type Nat = Bool
    type Zero = True
    type Succ[B <: Bool] = B#Not
  }
  trait IsOdd extends Nats {
    val booleans: Booleans; import booleans._
    type Nat = Bool
    type Zero = False
    type Succ[B <: Bool] = B#Not
  }

  // Some random implementation for booleans:
  //
  //   True  ~ Int
  //   False ~ String
  //
  // Need dotties real union types here!
  object boolImpl extends Booleans {
    sealed trait Bool <: {
      type Not <: Bool
      type Value
      def value: Value
    }
    case class True(value: Int) extends Bool {
      type Not = False;
      type Value = Int
    }
    case class False(value: String) extends Bool {
      type Not = True;
      type Value = String
    }
  }


  // Putting everything together

  object evenClient extends Client { outer =>
    object nats extends IsEven {
      val booleans = outer.booleans
    }
    val booleans = boolImpl

    val _x: String = x.value
    val _y: Int = y.value
  }
  
  
  // Tupling of Type Algebras
  
  trait Tuple { type _1; type _2 }
  type &&[L, R] = Tuple { type _1 = L; type _2 = R }

  trait TupleAlg <: Nats {
    val n1: Nats
    val n2: Nats

    type Nat            = Tuple { type _1 <: n1.Nat; type _2 <: n2.Nat }
    type Zero           = n1.Zero && n2.Zero
    type Succ[N <: Nat] = n1.Succ[N#_1] && n2.Succ[N#_2]
  }

  object tupleClient extends Client { outer =>
    object even extends IsEven {
      val booleans = outer.booleans
    }
    object odd extends IsOdd {
      val booleans = outer.booleans
    }
    val booleans = boolImpl

    object nats extends TupleAlg {
      val n1 = even
      val n2 = odd
    }

    implicitly[T1#_1#Value =:= String]
    implicitly[T1#_2#Value =:= Int]
    
    implicitly[T2#_1#Value =:= Int]
    implicitly[T2#_2#Value =:= String]
  }
}