Home

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?

By Bryn Keller at 2004-07-19 16:19 | Functional | Type Theory | other blogs | 11462 reads

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.

By Ehud Lamm at Mon, 2004-07-19 20:11 | login or register to post comments

Tip

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

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

By Mark Evans at Tue, 2004-07-20 02:54 | login or register to post comments

PDF version also on-line

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

By Dave Menendez at Tue, 2004-07-20 03:39 | login or register to post comments

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

By Jim Apple at Wed, 2004-07-21 20:09 | login or register to post comments

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.
By Jim Apple at Fri, 2004-07-23 18:13 | login or register to post comments

NVU

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

Does Nvu work on Windows?

By Bryn Keller at Wed, 2004-07-21 23:11 | login or register to post comments

Re: NVU

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

By Mark Evans at Sun, 2004-07-25 04:21 | login or register to post comments