Yitzchak Gale wrote:
Eric Mertens wrote:
(but I've had my head in Agda lately)
Indeed, coming across this problem tempted me to abandon the real world and take refuge in Agda.
Wow, so simple, and no higher-rank types! This is the best solution yet. I am now truly in awe of the power of GADTs.
Just for reference, here a full version of my solution http://hpaste.org/44503/software_stack_puzzle_annotat It's almost the same as Eric's solution except that he nicely fused the dropC and takeC functions into runLayers , thereby eliminating the need for existential quantification. However, note that GADTs subsume higher-rank types. With data Exists f where Exists :: f a -> Exists f you can always encode them as exists a. f a = Exists f forall a. f a = (exists a. f a -> c) -> c = (Exists f -> c) -> c Regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com