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.