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.
http://hpaste.org/44469/software_stack_puzzle
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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
