How to use GADTs in Hugs

Question

I'd like to write a Haskell program that uses GADTs interactively on a platform not supported by GHCi (namely, GNU/Linux on mipsel). The problem is, the construct that can be used to define a GADT in GHC, for example:

data Term a where
    Lit :: Int ->  Term Int
    Pair :: Term a -> Term b -> Term (a,b)
    ...

doesn't seem working on Hugs.

1. Can't GADTs really be defined in Hugs? My TA at a Haskell class said it was possible in Hugs, but he seemed unsure.
2. If not, can GADT be encoded by using other syntax or semantics supported by Hugs, just as GADTs can be encoded in ocaml?

Diathermic

@is7s: how can I do that? Currently I run hugs with option -98. – Diathermic

Folks -- GHC-specific language extensions are not available in Hugs. – Fortin

Answer 1

GADTs are not implemented in Hugs.

Instead, you should use a port of GHC to mips if you are attempting to run code using GADTs. Note that you won't be able to use ghci on all platforms, due to lack of bytecode loading on more exotic architectures.

Fortin

Thanks, I will use ghc once I finish writing my code. However, when you're halfway it might be useful to have an interpreter. Do you have an answer to the question 2, about encoding GADTs in Haskell'98? – Diathermic

Some GADT examples can be translated to type classes, martijn.van.steenbergen.nl/journal/2009/11/12/… – Fortin

Answer 2

Regarding your question 2 (how to encode GADT use cases in Haskell 98), you may want to look at this 2006 paper by Sulzmann and Wang: GADTless programming in Haskell 98.

Like the OCaml work you're referring to, this works by factoring GADTs through an equality type. There are various ways to define equality type; they use a form of Leibniz equality like for OCaml, which allows to substitute through any application of a type operator at kind * -> *.

Depending on how a given type checker reason about GADT equalities, this may not be expressive enough to cover all examples of GADTs: the checker may implement equality reasoning rules that are not necessarily captured by this definition. For example, a*b = c*d implies a = c and b = d: this form of decomposition does not come if you only apply type constructors at kind * -> *. Later in 2010, Oleg discussed how you can use type families to apply "type deconstructors" through Leibniz equality, gaining decomposition properties for this definition -- but of course this is again outside Haskell 98.

That's something to keep in mind for type system designers: is your language complete for leibniz equality, in the sense that it can express what a specialized equality solver can do?

Even if you find an encoding of the equality type that is expressive enough, you will have very practical convenience issues: when you use GADTs, all uses of equality witness are inferred from type annotations. With this explicit encoding you'll have much more work to do.

Finally (no pun intended), a lot of use cases of GADTs can be equally expressed by tagless-final embeddings (again by Oleg), that IIRC can often be done in Haskell 98. The blog post by Martin Van Steenbergen that dons points to in its reply's comment is in this spirit, but Oleg has considerably improved this technique.

Beslobber