
27 May
2010
27 May
'10
9:11 p.m.
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