
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