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

[Ivan Miljenovic]

On 28 May 2010 15:18, wren ng thornton <wren at freegeek.org> wrote:
> 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.

I can see a slight distinction between them, based upon when the
quantification occurs (the former returns a function that work on all
t, the latter will do that encoding for all t).

For most purposes there is no difference, but IIUC the former will let
you do hlist style stuff post-encoding whilst the latter doesn't.

-- 
Ivan Lazar Miljenovic
Ivan.Miljenovic at gmail.com
IvanMiljenovic.wordpress.com