Why only inference in type checking?

Philip K.F. Hölzenspies p.k.f.holzenspies at utwente.nl
Thu Oct 18 07:15:53 EDT 2007


Dear All,

A while ago, I had trouble understanding the coverage condition and I
raised a question on this mailing list. Help was swift and adequate,
especially the reference to the paper entitled "Understanding
Functional Dependencies via Constraint Handling Rules" was very
useful.

However, having considered the problem of non-termination of the type
checker, I can't help but wonder why the type checker is "inference
only." From the paper mentioned above, consider the following example:


class Mul a b c | a b -> c where
  (*) :: a -> b -> c

type Vec b = [b]
instance Mul a b c => Mul a (Vec b) (Vec c) where ...

f b x y = if b then (*) x [y] else y


For actual arguments of f, there is no issue whatsoever with
decidability. The type checker in my brain uses unification, i.e.
top-down. The type checker in GHC uses inference, i.e. bottom-up. Why
inference potentially suffers from non-termination for this program, I
understand.

My question is this: Is there a reason why type checking in GHC is
inference-only, as opposed to a meet-in-the-middle combination of
unification and inference? Would the type checker use both unification
and inference (let's say alternating evaluation of both), the number
of programs for which termination can be guaranteed is considerably
larger - if I'm not mistaken, but I may very well have gotten it
wrong.

Regards,
Philip

PS.
I realize that for this dependent typing scenario is useless once Type
Families are here. I can't wait for a GHC with TFs. I raise this
question, simply to understand why inference was chosen exclusively.


More information about the Glasgow-haskell-users mailing list