GADTs in the wild

Christian Maeder Christian.Maeder at
Fri Aug 17 12:59:39 CEST 2012

Am 15.08.2012 23:13, schrieb Yitzchak Gale:
> But in my opinion, by far the best solution, using only
> GADTs, was submitted by Eric Mertens:
> Eric's solution could now be simplified even further
> using data kinds.

Find attached a version (based on Eric's solution) that uses only 

data Fun a c = First (a -> c)
   | forall b . Serializable b => Fun b c :. (a -> b)

instead of:

data Fun :: * -> * -> * where
    Id   :: Fun a a
    (:.) :: Serializable b => Fun b c -> (a -> b) -> Fun a c

The main problem seems to be to create a dependently typed list of 
functions (the type of the next element depends on the previous one)
For such a list the element type depends on the index, therefore it 
seems not possible to define take and drop over "Fun a c" and compose it 

   serialize . flatten (take n fs) . deserialize

(as would be easily possible with functions of type "a -> a")

Cheers Christian

> Yitz

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Puzzle.hs
Type: text/x-haskell
Size: 1701 bytes
Desc: not available
URL: <>

More information about the Glasgow-haskell-users mailing list