[Haskell] Re: Polymorphic types without type constructors?
oleg at pobox.com
oleg at pobox.com
Tue Feb 1 22:36:00 EST 2005
> 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).
More information about the Haskell
mailing list