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