Recent Posts

Lambdalog

Sean Seefried's programming blog

22 Nov 2011

Haskell GADTs in Scala

This is an updated version of an earlier post. Owing to a comment by Jed Wesley-Smith I restructured this post somewhat to introduce two techniques for programming with GADTs in Scala. Thanks also go to Tony Morris.

First we’ll start with a fairly canonical example of why GADTs are useful in Haskell.

Here we have defined a data structure that represents the abstract syntax tree (AST) of a very simple arithmetic language. Notice that it ensures terms are well-typed. For instance something like the following just doesn’t type check.

I have also provided a function eval that evaluates terms in this language.

In Scala it is quite possible to define data structures which have the same properties as a GADT declaration in Haskell. You can do this with case classes as follows.

But how do we implement eval. You might think that the following code would work. I mean, it looks like the Haskell version, right?

Unfortunately for us, this doesn’t work. The Scala compiler is unable to instantiate the type Exp[A] to more specific ones (such as LitInt which extends Exp[Int])

3: constructor cannot be instantiated to expected type;
  found   : FailedExp.LitInt
  required: FailedExp.Exp[A]
    case LitInt(i)       => i
        ^

There are two solutions to this problem.

Solution 1: The object-oriented way

You must write eval the object-oriented way. The definition of eval gets spread over each of the sub-classes of Exp[A].

Solution 2: The functional Haskell-like way

Personally I don’t like the OO style as much as the Haskell-like style. However, it turns out that you can program in that style by using a companion object.

Ah, much better. But why does this work when the previous style doesn’t? The problem is that the constructors are not polymorphic. In Haskell-speak the type is:

not

The second solution is subtly different. Method evalAny is polymorphic but its type is instantiated to that of the value of whatever it is called on. For instance evalAny when called on LitInt(42) equates type variable A with Int. It can then correctly deduce that it does indeed take a value of Exp[Int] and produce a value of Int.

Tagged as: Haskell, Scala, GADTs.

blog comments powered by Disqus