[Haskell-cafe] A practical Haskell puzzle

Heinrich Apfelmus 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.
>> 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


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

Heinrich Apfelmus


More information about the Haskell-Cafe mailing list