[Haskell-cafe] A practical Haskell puzzle
apfelmus at quantentunnel.de
Fri Mar 4 14:38:30 CET 2011
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
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
More information about the Haskell-Cafe