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

[C. McCann]

On Thu, May 27, 2010 at 9:11 PM, Stefan Monnier
<monnier at iro.umontreal.ca> wrote:
> I.e. to make such an encoding really usable, you need "deep
> polymorphism" (which GHC supports just fine, but which is not part of
> the Haskell standard).

Ah, yes, and thank you for pointing that out. My message involved a
great deal of hand-waving that I neglected to clearly identify as
such. The same caveat of course applies to most Church encodings. For
instance, the proper type of a (recursive) encoded list would be:

type ChurchList a = ∀t. t -> (a -> t -> t) -> t

...where "a" is fixed as the type of the list elements. Thus, "cons"
ought to look something like this charming type:

cons :: ∀a. a -> (∀t. t -> (a -> t -> t) -> t) -> (∀t. t -> (a -> t -> t) -> t)

For extra fun, try writing an instance such as:

instance (Show a) => Show (ChurchList a) where [...etc.]

...at which point, perhaps, we remind ourselves that the language is
named "Haskell", not "Alonzo", and drop the whole matter.

- C.