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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
