| 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 meta-type variables representing as-yet-unknown types;
as the algorithm runs these meta-type 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, higher-rank 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 for-all 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 user-written types. But if you could instantiate a
type variable with a polytype, then for-alls could occur to the right of
an arrow as a result of the instantiation.
My current plan is to throw out the prenex-polytype 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
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
