[Haskell-cafe] Re: Chuch encoding of data structures in Haskell

[Stefan Monnier]

> churchedBool :: t -> t -> t

Important detail: the precise type is "∀t. t → t → t".

> encodeBool x = \t e -> if x then t else e

So the type of encodeBool should be:

 Bool → ∀t. t → t → t

whereas Haskell will infer it to be

  ∀t. Bool → t → t → t

which means that a given object can only be eliminated to one type.
I.e. to make such an encoding really usable, you need "deep
polymorphism" (which GHC supports just fine, but which is not part of
the Haskell standard).


        Stefan