I have been thinking about using Haskell (extended with higher ranked polymorphism) to demonstrate to my colleagues some ideas in second-order lambda calculus. It turned out, however, I am puzzled by the type system myself. So I've written to seek for help. :)
I started with define Church numerals as
type N = forall a . (a -> a) -> a -> a
(The syntax above works only for GHC. In Hugs I would have to write type N a = (a -> a) -> a -> a and replace every N below with (forall a. N a)) I should have used newtype or data instead of a type synonym, but I wanted it to look more like seond-order lambda calculus so I tried to omit the constructor if possible.
Let us consider a simpler example than the type N.
f1:: (forall a. a->a) -> b -> b f1 g x = g x -- *P1> f1 id True -- True
foo:: forall c notimportant. (c->c) -> notimportant foo = undefined
If we try
*P1> foo f1
we get an error
<interactive>:1: Inferred type is less polymorphic than expected Quantified type variable `a' escapes Expected type: (a -> a) -> a -> a Inferred type: (forall a1. a1 -> a1) -> b -> b In the first argument of `foo', namely `f1' In the definition of `it': it = foo f1
And indeed: the type of `foo' says that its argument must be a function from some type `c' to exactly the same type. The function f1 has the type (forall a. a->a) -> (forall b. b->b) The question then becomes: is (forall a. a->a) the same as (forall b. b->b) ? Not to Haskell. That would require a higher-order unification. However, not everything is lost. There is a way to convince GHC that the two quantified types are really the same. We just need a suitable envelope. Nominal equivalence does come handy sometimes. Here's the code
{-# OPTIONS -fglasgow-exts #-}
module P1 where
import Prelude hiding (succ)
newtype N = N (forall a . (a -> a) -> a -> a) un (N x) = x
zero :: N zero = N ( \f a -> a )
succ :: N -> N succ n = N ( \f a -> f (un n f a) )
one:: N one = succ zero
add, mul :: N -> N -> N add m n = N( \f a -> un m f (un n f a) ) mul m n = N( \f a -> un m (un n f) a )
exp :: N -> N -> N exp m n = un n (mul m) one
exp2 :: N -> N -> N exp2 m n = N (\f a -> un n (un m) f a)
test1 = un (P1.exp two three) (+1) 0 where two = succ one three = succ two
test2 = un (P1.exp2 two three) (+1) 0 where two = succ one three = succ two
I must note that in this code, one may not replace N (...) with N $ ( ...). This is yet another case where ($) is not the same as an application with a lower precedence. The code has a redeeming feature: the data constructor N marks the places of explicit big-lambda introductions. The function 'un' marks the places of explicit big lambda eliminations (that is, type applications).