Wednesday, June 9, 2010

GADTs in Scala

It looks like ordinary Scala case classes can express GADTs. Here's an example:
trait Expr[A] 
case class I(i: Int) extends Expr[Int]
case class B(b: Boolean) extends Expr[Boolean]
case class Add(a: Expr[Int], b: Expr[Int]) extends Expr[Int]
We can define an evaluation function with the type Expr[A] => A:
def eval[A](e: Expr[A]): A = e match {
case I(i) => i
case B(b) => b
case Add(a,b) => eval(a) + eval(b)
This all compiles and typechecks, and has the expected behavior: Add(I(1), B(false)) is a type error, eval(I(22)) results in 22, etc.

I haven't played with this much, so I wonder if there's any situations where the Scala GADTs behave differently than Haskell's.


Luke Palmer said...

Not quite. Scala does not do type refinement. For example, contrast:

trait Eq[A,B]
case class Refl[A]() extends Eq[A,B]

object Main {
def eval[A](a : A, eq : Eq[A,Int]) : A = eq match {
case Refl() => 1 + a


data Equal a b where
Refl :: Equal a a

eval :: a -> Equal a Int -> a
eval x Refl = 1 + x

Paul Chiusano said...

@Luke - did you mean for Refl[A] to extend Eq[A,A] in your Scala example?

Luke Palmer said...

Ah, yes I did, thanks. It still doesn't compile.

Paul Chiusano said...

@Luke - Hmm... interesting. Thanks for the comment. I'm trying to figure out how limiting this is... can you provide a more illustrative example or maybe just talk about how that facility gets used in Haskell?

Aaron Turon said...

There's a nice paper, "Generalized algebraic data types and object-oriented programming," that looks at this kind of encoding in more detail: