[Haskell] Re: Polymorphic types without type constructors?

[oleg at pobox.com]

> 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).