Wobbly types

Wobbly types: type inference for generalised algebraic data types


Simon Peyton Jones, Geoffrey Washburn, and Stephanie Weirich.
July 2004
Postscript

Generalised algebraic data types (GADTs), sometimes known as "guarded recursive data types" or "first-class phantom types", are a simple but powerful generalisation of the data types of Haskell and ML. Recent works have given compelling examples of the utility of GADTs, although type inference is known to be difficult.

It is time to pluck the fruit. Can GADTs be added to Haskell, without losing type inference, or requiring unacceptably heavy type annotations? Can this be done without completely rewriting the already-complex Haskell type-inference engine, and without complex interactions with (say) type classes? We answer these questions in the affirmative, giving a type system that explains just what type annotations are required, and a prototype implementation that implements it. Our main technical innovation is wobbly types, which express in a declarative way the uncertainty caused by the incremental nature of typical type-inference algorithms.

Edit: Made the title into a hyperlink, as the "Postscript" link could easily get lost in a sea of blue text...

Edit 2:Quoted the article with a plain-ol' <blockquote> instead. Better?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Ha!

It seems Geoffrey Washburn has a blog.

Tip

the "Postscript" link could easily get lost in a sea of blue text...

Links accept the style attribute, too. Nvu is very good.

PDF version also on-line

There are links to versions in various formats at Geoffrey Washburn's research page.

Why does this fail to simulate GADTs

Contructing terms is fine, but pattern mathcing fails:

{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
 
data Term a = forall b . (EqType a b, EqType b Int) => Lit Int
            | forall b . (EqType a b, EqType b Int) => Inc (Term Int)
            | forall b . (EqType a b, EqType b Bool) => IsZ (Term Int)
            | If (Term Bool) (Term a) (Term a)
            | forall b . Fst (Term (a,b))
            | forall b . Snd (Term (b,a))
            | forall b c . (EqType a (b,c))=> Pair (Term b) (Term c)
 
class EqType a b | a->b, b->a
instance EqType a a

Because phantom types are not first class

First-Class Phantom Types, by James Cheney

This particular case, found in the wobbly types paper, can be simulated by

newtype Equal a b = Equal (forall f . f a -> f b)
cast :: Equal a b -> (a -> b)
cast (Equal f) = f id
                                                                                                                                            
data Term a = Lit Int (Equal Int a)
            | Inc (Term Int) (Equal Int a)
            | IsZ (Term Int) (Equal Bool a)
            | If (Term Bool) (Term a) (Term a)
            | forall b . Fst (Term (a,b))
            | forall b . Snd (Term (b,a))
            | forall b c . Pair (Term b) (Term c)  (Equal (b,c) a)
                                                                                                                                            
eval :: Term a -> a
eval (Lit x eq) = cast eq x
eval (Inc x eq) = cast eq ((eval x) + 1)
eval (IsZ x eq) = cast eq ((eval x) == 0)
eval (If x y z) = if (eval x) then (eval y) else (eval z)
eval (Fst x) = case eval x of
               (y,_) -> y
eval (Snd x) = case eval x of
               (_,y) -> y
eval (Pair x y eq) = cast eq (eval x, eval y)
although the above technical report indicates that there are some cases, like treis, that can't be simulated by this method.

NVU

Links accept the style attribute, too. Nvu is very good.

Does Nvu work on Windows?

Re: NVU

Yes, it's cross-platform by virtue of Mozilla.