[Haskell] MPTCs and type inference
Andreas Rossberg
rossberg at ps.uni-sb.de
Tue Apr 26 09:42:45 EDT 2005
Thanks for the detailed explanation that helped clearing up the smog in
my head. I reckoned that once more the MR was to blame, at least for
part of it.
>>>>in particular, when I compare with the single parameter case:
>>>>
>>>> class C a where fc :: a -> a -> ()
>>>>
>>>> c1 x = let p = fc x in ()
>>>> c2 x = let p y = fc x y in ()
>>>>
>>>>where
>>>>
>>>> c1 :: C a => a -> ()
>>>> c2 :: C a => a -> ()
>>>>
>>>>is inferred, as I would expect.
>
> The inference steps for this case are much the same except, that the
> inferred type for "p" now will be: "a -> ()", provided that we can
> solve the constraint "C a". Because we have assumptions about "a" in
> the environment (namely it is mentioned in the type of the varible
> "x") we cannot generalize the type of "p". It therefore remains
> monomorphic, and the constraint "C a" is propagated to the type of
> "c2".
To be more precise, p is not polymorphic *in the variables mentioned by
the constraint* - the overall type of p could still be polymorphic,
without changing the outcome.
My understanding now is as follows: a constraint is captured by a
declaration if at least one of the type variables mentioned in the
constraint is generalised in the respective type scheme. Is that a
correct interpretation?
Of course, this is not the only possible rule. Alternatively,
generalisation could always capture *all* unresolved constraints. For
example, the type of p in c2 could be C a => a->() without a being
quantified. That looks a bit more uniform in the face of MPTCs and would
allow more programs, because contexts induced by dead code in form of an
unused declaration could be forgotten consistently, not just when some
of its free variables happen to be bound by a local quantifier.
--
Andreas Rossberg, rossberg at ps.uni-sb.de
Let's get rid of those possible thingies! -- TB
More information about the Haskell
mailing list