GADTs in the wild

[Christian Maeder]

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:
>
> http://hpaste.org/44469/software_stack_puzzle
>
> Eric's solution could now be simplified even further
> using data kinds.

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

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 
like

   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: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120817/d7f540c1/attachment.hs>