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$ Sep 11, 2013 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, 2013 at 6:06

1 Answer 1


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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