# Implementation of datatypes in Haskell?

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.

• 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. – Jonathan Gallagher Sep 11 '13 at 0:14
• 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. – jbapple Sep 18 '13 at 6:06