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