Talk:Haskell/GADT

From Wikibooks, the open-content textbooks collection

[edit] About Example: Trouble with GADTs

We can define SafeList in the following manner, without such troubles:

data Empty
data NonEmpty

data SafeList :: * -> * -> * where
     Nil  :: SafeList x Empty
     Cons :: x -> SafeList x y  -> SafeList x z

safeHead :: SafeList x NonEmpty -> x
safeHead (Cons x _) = x

-- bad typed as before
--bad = safeHead Nil

-- OK
silly 0 = Nil
silly 1 = Cons 1 Nil

Nice. Thanks. Can you please update the page with some discussion? -- Kowey 15:07, 2 July 2007 (UTC)

That doesn't buy you much, though:

safeHead (silly 1)

still fails.

[edit] About Example: Existential Types

The bits about TE2/TG2 talk about "heterogenous lists", but that's inaccurate. Each TE2/TG2 instance contains a homogeneous list of b's (the existentially-quantified type). Of course, each instance may use a different b. (Paul Steckler)

[edit] Poorly written, but gets the point across

I think somebody made this point about this (stub) article on #haskell. Criticism gratefully received! Any takers? For what it's worth, I always found the examples used explaining GADT to be a little hard to understand (it took quite a while for them to really sink in). Some nice new examples would be useful. Also Ganesh's talk in LondonHUG seems to do a pretty good job explaining GADTs. Worth borrowing some ideas from him -- Kowey (talk) 09:13, 25 February 2008 (UTC)

I had some time and digged up examples:

• Ganesh's talk in LondonHUG GADTs for patches.
• SPJ - type inference for GADTs (rewritten version of the wobbly paper). Features the standard expression evaluator example.
• LtU - Prototyping new monads Term implementation for the state monad.
• Hinze - Fun with Phantom Types Strongly typed printf. (It's possible to do that without GADTs, though). Generic programming (= representing types as values).
• This wikibook: safe lists.
• Fixed size vectors/matrices. Other invariants like AVL or red-black trees.

So, most examples emphasize safety, but I think the one that does not is the most compelling one. Its basic message is: with GADTs, pretty much every abstract data type has a term-implementation, that can be used to cook up its implementation. That's enough to warrant GADTs in the language and makes a good starting point for the wikibook. Unfortunately, it's the state monad, which may create unwanted associations in the reader's mind... I wonder whether there is a different example without troubling ballast.

Btw, I think the word "safety" should be replaced by "more precise types" or "more fine-grained types" or something; just a feeling.

-- apfeλmus 17:25, 25 February 2008 (UTC)

More example goodness:

• LtU - How are GADTs useful in practical programming?. Meta-resource.
• Augustsson,Petersson - Silly Type Families Parser combinators as GADTs, they're not monadic. The intention is to automatically left-factor easy grammars, you need an (G)ADT for that. But I think that these combinators can be recast as applicative functors, eliminating the need for Seq :: Grammar a -> Grammar b -> Grammar (a,b) which forces the extension to GADTs. Not sure whether left-factoring is still feasible then, though. If it ever was...
• Yampa GADTs enable optimizations by cutting down dynamic checks, or so I hear.
• Contracts for functional programming. An embedded DSL for dynamically checking constraints ("contracts"), i.e. more invariants but dynamically checked. GADTs make the implementation easy / make it possible at all.

-- apfeλmus 21:14, 6 March 2008 (UTC)