GADT

Generalized Abstract Data Types

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)))
Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-ShareAlike 3.0 License