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

[wren ng thornton]

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