Scala GADTs

GADTs.scala

/* http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#gadt
Generalized Algebraic Datatypes in Scala */

trait Term[A]
case class Lit(x: Int) extends Term[Int]
case class Succ(x: Term[Int]) extends Term[Int]
case class IsZero(x: Term[Int]) extends Term[Boolean]
case class If[A](guard: Term[Boolean], t: Term[A], y: Term[A]) extends Term[A]
case class Pair[A, B](x: Term[A], y: Term[B]) extends Term[(A,B)]
      
def eval[A](x: Term[A]): A = x match {
  case Lit(i)       => i
  case Succ(t)      => 1 + eval(t)
  case IsZero(t)    => eval(t) == 0
  case If(b,e1, e2) => if (eval(b)) eval(e1) else eval(e2)
  case Pair(e1, e2) => (eval(e1), eval(e2))
}