28 May
2010
28 May
'10
1:18 a.m.
Stefan Monnier wrote:
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
Those are the same type.
which means that a given object can only be eliminated to one type.
No, the t is universally quantified just fine. Perhaps you're thinking of the need for rank-2 polymorphism in functions which take Church-encoded arguments? -- Live well, ~wren