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

[wren ng thornton]

Ivan Miljenovic wrote:
> 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).

The isomorphism in System F:

     in : (∀t. Bool → t → t → t) → (Bool → ∀t. t → t → t)
     in f = \b. /\t. f @t b


     out : (Bool → ∀t. t → t → t) → (∀t. Bool → t → t → t)
     out g = /\t. \b. g b @t


If you're using the raw System F, then there's a slight difference ---as 
there always is between isomorphic things which are non-identical--- but 
that difference is not theoretically significant. If you're using a 
higher-level language like Haskell, then the conversions are done for 
you, so there's even less difference.

The expression 1+1 is distinct from 2: it has a different representation 
in memory, it takes a different number of steps to normalize, etc. 
Sometimes these differences are important for engineering (e.g., dealing 
with space leaks), but they're rarely significant for theory.

-- 
Live well,
~wren