GADTs and pedagogy was Re: GADTs and fundeps

[Shae Matijs Erisson]

"Simon Peyton-Jones" <simonpj at microsoft.com> writes:

> You are quite right.  Indeed GADTs don't interact properly with type
> classes at all, let alone functional dependencies, I'm afraid.   I
> decided to pause and release before attending to this; it's not trivial
> to do it right.

I haven't tripped over anything in particular, but I have been helping the Pugs
developers[1] with Haskell. Autrijus Tang pointed out that the type examples in
the HaskellDemo[2] are easier for new users with GADTs.

HaskellDemo has this:
data Temp = Cold | Hot
data People = Person Name Age

But new users find this much easier to understand:
data Temp where 
    Cold :: Temp
    Hot  :: Temp

data People where 
    Person :: Name -> Age -> People

I'd guess GADTs are clearer because type signatures like this put constructors
into the mental category of 'just another function'.
They also make the difference between constructor and type names very clear.
(This is another common newbie confusion.)

I doubt pedagogics was an important part of your goal with GADTs, but now
several people wish that "deriving Show" worked so that GADTs could be used for
everything.

[1] http://pugscode.org/
[2] http://www.haskell.org/hawiki/HaskellDemo
-- 
Programming is the Magic Executable Fridge Poetry, | www.ScannedInAvian.com
It is machines made of thought, fueled by ideas.   | -- Shae Matijs Erisson