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

Ivan Miljenovic wrote:

On 28 May 2010 15:18, wren ng thornton 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