[Haskell-cafe] Fwd: Questions about lambda calculus

[wren ng thornton]

On 11/10/10 9:18 AM, Max Bolingbroke wrote:
> On 10 November 2010 12:49, Patrick LeBoutillier wrote:
>> I'm a total newbie with respect to the lambda calculus. I tried
>> (naively) to port these examples to Haskell to play a bit with them:
>
> You can give type signatures to your first definitions like this:
>
> {-# LANGUAGE RankNTypes #-}


The secret is that Church encodings of data types only work 
straightforwardly in the untyped lambda calculus, where every term 
*does* have the infinite type a ~ (a->a). Once you move to a typed 
lambda calculus like Haskell, those types are rejected. You can get 
pretty far with Church Booleans before things break, but Church natural 
numbers break very quickly.

The sneaky bit is that Church encodings (though intended for the untyped 
lambda calculus) can be given valid types in System F, aka -XRankNTypes. 
Unfortunately the types of System F cannot, in general, be inferred 
automatically. So to preserve type inference, most functional languages 
will limit the kinds of polymorphism allowed to the Hindley--Milner 
subset of System F, which excludes most Church encodings.

The moral of the story is, you need to enable -XRankNTypes and you need 
to provide explicit type signatures (or else use newtypes to the same 
effect).

-- 
Live well,
~wren