[Haskell-cafe] Mysterious fact

[Dan Doel]

On Monday 01 November 2010 6:40:30 pm Jeremy Shaw wrote:
> Looks a lot like Church encoding to me:
> 
> http://en.wikipedia.org/wiki/Church_encoding
> 
> It was first discovered by the guy who invented lambda calculus :p

Also, if you're interested in this, you can read Proofs and Types by Girard 
(not an easy read). In it, (I think) he notes, and probably proves, that you 
can encode any inductive type in System F (which is relatively close to 
Haskell with rank-n types) by this method (that is, it has the right types; of 
course it works in the untyped lambda calculus, too, but not in, say, the 
simply typed lambda calculus).

You can also encode coinductive types:

  nu F = exists s. s * (s -> F s)

  exists s. T[s] = forall r. (forall s. T[s] -> r) -> r

-- Dan