[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,
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.
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
More information about the Haskell
mailing list