GADT

### Generalized Abstract Data Types

- http://www.haskell.org/haskellwiki/Generalised_algebraic_datatype
- http://hackage.haskell.org/trac/haskell-prime/wiki/GADTs
- http://hackage.haskell.org/trac/haskell-prime/wiki/ExistentialQuantification

It provide us to have a better way to represent data type, which a constructor has a non standard type. We can create a generic type for different types.

In Haskell:

`data Foo a = Foo1 a | Foo2 Int Int`

we can get two constructor

```
Foo1 :: a->Foo a
Foo2 :: Int -> Int -> Foo a
```

The "generalize" in GADT means the result of constructor can be an instance of Foo a.

Ex:

```
data Foo a where
Foo1 :: a -> Foo ()
Foo2 :: a->Int -> Foo a
```

The argument a can have some more informations which can be used later.

Ex:

```
data Expr a where
Num :: Int -> Expr Int
Plus :: Expr Int -> Expr Int -> Expr Int
T :: Expr Bool
...
```

We can make sure Plus T (Num 3) is invalid.

We can see the following example which merge all other types into one "Parser tok a".

```
data Parser tok a where
Zero :: Parser tok ()
One :: Parser tok ()
Check :: (tok -> Bool) -> Parser tok tok
Satisfy :: ([tok] -> Bool) -> Parser tok [tok]
Push :: tok -> Parser tok a -> Parser tok a
Plus :: Parser tok a -> Parser tok b -> Parser tok (Either a b)
Times :: Parser tok a -> Parser tok b -> Parser tok (a,b)
Star :: Parser tok a -> Parser tok [a]
parse :: Parser tok a -> [tok] -> Maybe a
-- Zero always fails.
parse Zero ts = mzero
-- One matches only the empty string.
parse One [] = return ()
parse One _ = mzero
-- Check p matches a string with exactly one token t such that p t holds.
parse (Check p) [t] = if p t then return t else mzero
parse (Check p) _ = mzero
-- Satisfy p any string such that p ts holds.
parse (Satisfy p) xs = if p xs then return xs else mzero
-- Push t x matches a string ts when x matches (t:ts).
parse (Push t x) ts = parse x (t:ts)
-- Plus x y matches when either x or y does.
parse (Plus x y) ts = liftM Left (parse x ts) `mplus` liftM Right (parse y ts)
-- Times x y matches the concatenation of x and y.
parse (Times x y) [] = liftM2 (,) (parse x []) (parse y [])
parse (Times x y) (t:ts) =
parse (Times (Push t x) y) ts `mplus`
liftM2 (,) (parse x []) (parse y (t:ts))
-- Star x matches zero or more copies of x.
parse (Star x) [] = return []
parse (Star x) (t:ts) = do
(v,vs) <- parse (Times x (Star x)) (t:ts)
return (v:vs)
token x = Check (== x)
string xs = Satisfy (== xs)
p = Times (token 'a') (token 'b')
p1 = Times (Star (token 'a')) (Star (token 'b'))
p2 = Star p1
blocks :: (Eq tok) => Parser tok [[tok]]
blocks = Star (Satisfy allEqual)
where allEqual xs = and (zipWith (==) xs (drop 1 xs))
evenOdd = Plus (Star (Times (Check even) (Check odd)))
(Star (Times (Check odd) (Check even)))
```

page revision: 5, last edited: 03 Dec 2007 18:58