[Haskell-cafe] A practical Haskell puzzle

[Heinrich Apfelmus]

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