[Haskell] Polymorphic types without type constructors?
Simon PeytonJones
simonpj at microsoft.com
Wed Feb 2 04:09:33 EST 2005
 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] (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

 (SLPJ: note that N is a polymorphic type)
You have it exactly right. The key word is "predicative". GHC has a
predicative type system, that only allows you to instantiate a type
variable with a monotype, not a polytype. An impredicative system
(which is the one you want here) is more expressive, but it makes type
inference very much more difficult.
The algorithm is more difficult because type inference algorithms
usually work with metatype variables representing asyetunknown types;
as the algorithm runs these metatype variables are gradually
substituted with their final type. But if this gradual substitution can
involve polymorphic types, then type instantiation should have occurred
earlier.... Try it yourself.
Difficult is not impossible. If you are interested, look at MLF, a
fantastic piece of work from INRIA (Remy & Le Botlan), that describes
type inference for an impredicative, higherrank type system.
 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.
Your intuition is good. Somehow, one might expect that if you told GHC
*at the moment of instantiation* what to instantiate to, it ought to
work, because there is no guessing involved. For example you ought to
be able to say
exp2 :: N > N > N
exp2 n m = n {N} m
Here, the {N} is a type argument to n.
But I have not implemented this (yet). The main difficulty I
encountered when thinking about is this. GHC uses prenex polytypes. If
you write
f :: Int > (forall a. a>a)
GHC behaves as if you'd written
f :: forall a. Int > a > a
That is, GHC's types never have a forall to the right of an arrow.
(You can read about this in "Practical type inference for higher rank
types" on my home page.) Currently, this is a simple syntactic
transformation on userwritten types. But if you could instantiate a
type variable with a polytype, then foralls could occur to the right of
an arrow as a result of the instantiation.
My current plan is to throw out the prenexpolytype invariant, and find
another way to deal with the problem that pushed me that way in the
first place. Something like coloured type inference. I'm working on
that with Dimitrios Vytiniotis and Stephanie Weirich.
Anyway, thanks for an interesting example.
Simon
More information about the Haskell
mailing list