# [Haskell] Polymorphic types without type constructors?

Shin-Cheng Mu scm at ipl.t.u-tokyo.ac.jp
Tue Feb 1 20:20:44 EST 2005

```Hi,

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.

I could define addition and multiplication smoothly.

> zero :: N
> zero = \f -> \a ->  a

> succ :: N -> N
> succ n = \f -> \a -> f (n f a)

> add, mul :: N -> N -> N
> add m n = \f -> \a -> m f (n f a)
> mul m n = \f -> \a -> m (n f) a

But when it comes to exponential, GHCi complained about type
being not polymorphic enough.

> exp :: N -> N -> N
> exp m n = n (mul m) one

GHC said:
Inferred type is less polymorphic than expected
Quantified type variable `a' escapes
Expected type: ((a -> a) -> a -> a) -> (a -> a) -> a -> a
Inferred type: (forall a2. (a2 -> a2) -> a2 -> a2)
-> (a1 -> a1) -> a1 -> a1
In the application `mul m'
In the first argument of `n', namely `(mul m)'

On the other hand, there is another definition of exp

> exp2 :: N -> N -> N
> exp2 m n = n m

which would type check.

It seems to me that the difference is: in the case of the second
definition of exp, the type variable in N can be instantiated to
a monomorphic type (the same with add and mul).

exp2 = \m::N -> \n::N -> \f::(b -> b) -> \b::b ->
n [b->b] (m[b]) f b

(where square brackets denote type application)
while in the first exp, n::N is instantiated to a polymorphic type
(another N):

exp = \m::N -> \n::N -> \f::(b -> b) -> \b::b ->
(n[N] (mul m) one)[b] f b

I tried to add more type signatures to inform GHC of the fact
that n::N is to be instantiated to a polymorphic type. However
none of the attempts worked so far. I then noticed that in the
GHC User's Guide (Sec 7.4.9) it was written

"There is one place you cannot put a forall: you cannot
instantiate a type variable with a forall-type. So you cannot
make a forall-type the argument of a type constructor."

The examples followed are all about type constructors (for example
[forall a. a->a], a list of for-all's, is illegal). But is this
the reason why exp cannot be typed?

If so, is there a reason for such a restriction?

Thank you very much!

sincerely,
Shin-Cheng Mu

```