TypesAsValues.scala

/*
 * Encode a pair of examples from GADT and OOP (Generalized Algebraic Data Types and Object Oriented Programming), OOPSLA '05.
 */

//Part of Fig. 11. This is not complete, as it looks rather boring.

//A universe construction, that is, a representation of types.

trait Rep[T] {
  def eq(x: T, y: T): Boolean
//  def pretty(x: T): String
}

class IntRep extends Rep[Int] {
  def eq(x: Int, y: Int) = x == y
}

class BoolRep extends Rep[Boolean] {
  def eq(x: Boolean, y: Boolean) = x == y
}

class PairRep[A, B](val a: Rep[A], val b: Rep[B]) extends Rep[(A, B)] {
  def eq(x: (A, B), y: (A, B)) =
    //Not `x == y`; reuse the universe construction instead and write:
    a.eq(x._1, y._1) && b.eq(x._2, y._2)
}

//Fig. 12: sized lists. This encoding is also possible in Tim Sheard's
//Omega, since it's a standard application of GADTs; moreover, there
//it actually works.

//Type-level naturals
trait Nat 
class Zero extends Nat
class Succ[T <: Nat] extends Nat

//Equality, similar to =:= but more similar to propositional equality in Agda or Omega's Equal. Doesn't work so well.
sealed trait =::=[A, B]
class Refl[A] extends =::=[A, A]
object =::= {
  implicit def tpEquals[A]: A =::= A = new Refl[A]
}

trait List[+A, L] {
  def head[K <: Nat](implicit p: L =::= Succ[K]): A
  def tail[K <: Nat](implicit p: L =::= Succ[K]): List[A, K]

  def map[B](f: A => B): List[B, L]
  def zip[B](that: List[B, L]): List[(A, B), L]
}

case class Nil[A]() extends List[A, Zero] {
   def head[K <: Nat](implicit p: =::=[Zero,Succ[K]]): A = ???
     //The typechecker recognizes that p can't be Refl, but doesn't
     //recognize that the method simply can't be called; we have to
     //provide it anyway.
     /*p match {
       case v: Refl[a] => ???
     }*/
   def tail[K <: Nat](implicit p: =::=[Zero,Succ[K]]): List[A,K] = ???

   def map[B](f: A => B): List[B,Zero] = Nil()
   def zip[B](that: List[B,Zero]): List[(A, B),Zero] = Nil()
}

//Like Scala's Nil and not like in the paper, since this requires covariance which is not supported in the paper.
case object Nil2 extends List[Nothing, Zero] {
   def head[K <: Nat](implicit p: =::=[Zero,Succ[K]]): Nothing = ???
   def tail[K <: Nat](implicit p: =::=[Zero,Succ[K]]): List[Nothing, K] = ???

   def map[B](f: Nothing => B): List[B,Zero] = Nil2
   def zip[B](that: List[B,Zero]): List[(Nothing, B),Zero] = Nil2
}

case class Cons[A, L <: Nat](h: A, t: List[A, L]) extends List[A, Succ[L]] {
   def head[K <: Nat](implicit p: =::=[Succ[L], Succ[K]]): A = h
   def tail[K <: Nat](implicit p: =::=[Succ[L], Succ[K]]): List[A, K] =
       //t // This would not typecheck. However, this version does, exactly like in Agda:
       p match {
         case v: Refl[a] => t
       }

   def map[B](f: A => B): List[B, Succ[L]] =
     Cons(f(head[L]), tail[L] map f)
   def zip[B](that: List[B, Succ[L]]): List[(A, B), Succ[L]] =
     Cons((head[L], that.head[L]), tail[L] zip that.tail)
}