Why only inference in type checking?

[Simon Peyton-Jones]

Sorry to be slow replying.  I don't know how to give a fully satisfactory answer.  Partly it's that we want to do inference sometimes and checking sometimes.  Partly it's that local constraints" makes checking quite a bit harder (see our paper "Towards open type functions for Haskell" on my home page).  Partly it's that functional dependencies are much trickier than they look (see our paper "Understanding functional dependencies via Constraint Handling Rules" also on my home page.

But you are right.  Tom and Martin are (at this moment) working on a system that support both general top-level equations and arbitrary local constraints.

Simon

| -----Original Message-----
| From: Philip K.F. Hölzenspies [mailto:p.k.f.holzenspies at utwente.nl]
| Sent: 19 October 2007 09:38
| To: Simon Peyton-Jones
| Cc: glasgow-haskell-users at haskell.org
| Subject: Re: Why only inference in type checking?
|
| Dear Simon,
|
| You mentioned that GHC uses 'checking' when it knows the types. How
| this relates to 'unification', I don't know. It might very well be the
| same. Hopefully, the following example sheds a bit more light on what
| I mean (carefully nicked from Uktaad B'mal's "Beginning Faking It").
| Examples are many, including in the "Understanding FDs via CHRs"
| paper.
|
| -- Start example
|
| To define 'vectors,' we need to code the length of a list in a type.
| With the zero/successor notation for naturals, we can do this is data
| constructors without term-level constructors:
|
| data Z
| data S x
|
| Vector concatenation requires addition of these numerals. In Prolog
| terms:
|
| Add(zero, X, X).
| Add(s X, Y, s Z) :- Add X Y Z
|
| We can translate this to a type class as
|
| class Add a b c | a b -> c
| instance Add Z x x
| instance Add x y z => Add (S x) y (S z)
|
| -- End example
|
| Because of your paper I understand why the coverage condition is in
| place and why it fails for the last of these instance declarations.
| GHC will allow me to do this by saying allow-undecidable-instances.
| As you state in the paper, the three FD-conditions of Coverage,
| Consistency and Bound Variable are sufficient, but not (always)
| necessary.
|
| I see why the example above causes considerable problems for
| inference, but if I read these instance declarations as Horn clauses,
| I see no problem at all in checking any actual occurrence in a
| program, i.e. if I write a concatenation function for vectors that
| uses this class as a property of vectors, I don't see where a type
| checker, using Prolog-like unification, runs into difficulties.
|
| What I'm probably asking (it's hard to tell, even for me, sometimes),
| is whether there is something between a type checker that is
| guaranteed to terminate and throwing all guarantees with regards to
| decidability right out the window. Again, I might be completely
| mistaken about how GHC does this. In that case I would like to find
| out where I make a wrongful assumption.
|
| Regards,
| Philip