GADT for polymorphic list

Question

I am parsing a few statements of the form

v1 = expression1
v2 = expression2
...

I am using the State Monad and my state should be a pair of (String, Expr a), I really insist on having the expressions typed. I tried to implement the state as [PPair] where I define PPair by the GADT:

data PPair where
    PPair :: (String, Expr a) -> PPair

Once this line passed the compiler, I felt that I am doing something really really wrong. I suppressed the thought and went on coding. When I came to writing the code that would extract the value of the variable from the State, I realized the problem:

evalVar k ((PPair (kk, v)):s) = if k == kk then v else evalVar k s

I get:

Inferred type is less polymorphic than expected

which is quite expected. How do I work around this problem? I know I can solve it by breaking up the type over all candidate types a, but is there no neater way?

Answer 1

The problem is that there's no possible type evalVar can have:

evalVar :: String -> [PPair] -> Expr ?

You can't say ? is a, because then you're claiming your return value works for any value of a. What you can do, however, is wrap up "an Expr with an unknown type" into its own data type:

data SomeExpr where
  SomeExpr :: Expr a -> SomeExpr

or, equivalently, with RankNTypes rather than GADTs:

data SomeExpr = forall a. SomeExpr (Expr a)

This is called existential quantification. You can then rewrite PPair using SomeExpr:

data PPair = PPair String SomeExpr

and evalVar works out:

evalVar k (PPair kk v : xs)
  | k == kk = v
  | otherwise = evalVar k xs

(Of course, you could just use a [(String,SomeExpr)] instead, and the standard lookup function.)

In general, though, trying to keep expressions completely typed at the Haskell level like this is probably an exercise in futility; a dependently-typed language like Agda would have no trouble with it, but you'll probably end up running into something Haskell can't do quite quickly, or weakening things to the point where the compile-time safety you wanted out of the effort is lost.

That's not to say it never works, of course; typed languages were one of the motivating examples for GADTs. But it might not work as well as you want, and you'll probably run into trouble if your language has any non-trivial type system features like polymorphism.

If you really want to keep the typing, then I'd use a richer structure than strings to name variables; have a Var a type that explicitly carries the type, like this:

data PPair where
  PPair :: Var a -> Expr a -> PPair

evalVar :: Var a -> [PPair] -> Maybe (Expr a)

A good way to achieve something similar to this would be to use the vault package; you can construct Keys from ST and IO, and use Vault as a heterogeneous container. It's basically like a Map where the keys hold the type of the corresponding value. Specifically, I'd suggest defining Var a as Key (Expr a) and using a Vault instead of your [PPair]. (Full disclosure: I've worked on the vault package.)

Of course, you'll still have to map the variable names to the Key values, but you could create all the Keys right after parsing, and carry those around instead of the strings. (It'd be a bit of work to go from a Var to its corresponding variable name with this strategy, though; you can do it with a list of existentials, but the solution is too long to put in this answer.)

(By the way, you can have multiple arguments to a data constructor with GADTs, just like regular types: data PPair where PPair :: String -> Expr a -> PPair.)