In Haskell, are datatypes converted to the "Church encoding" i.e. folding the data type. For example, given

data N = Z | S N

in Haskell, it can be converted to its church encoding by

foldN Z z s = z
foldN (S n) z s = s (foldN z s n)

Where if we do foldN m, we get the church encoding:

\z s . s (  .... s n ... )

In Proofs and Types, Girard shows how this works for any inductive datatype. There are two questions I have: (1) is this actually how Haskell treats datatypes and (2) what is the equivalent construction for coinductive datatypes.

  • $\begingroup$ What I mean by question (1) is: does Haskell use this translation into System F in any way? Does any language use such a translation? It seems that there would be efficiency issues with doing this. $\endgroup$ – Jonathan Gallagher Sep 11 '13 at 0:14
  • $\begingroup$ Haskell is a language, not a specific compiler or interpreter, so different implementations could do different things. GHC does not do this. As you stated, there would be efficiency issues. $\endgroup$ – jbapple Sep 18 '13 at 6:06

To answer the question: No implementation of Haskell to my knowledge has ever represented datatypes as church encodings.

I believe that church-style encodings (or variants such as Scott encodings) work equally well for coinductive types.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.