Why only inference in type checking?
Simon PeytonJones
simonpj at microsoft.com
Wed Nov 7 08:11:21 EST 2007
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 toplevel 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 PeytonJones
 Cc: glasgowhaskellusers 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 termlevel 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 allowundecidableinstances.
 As you state in the paper, the three FDconditions 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 Prologlike 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
More information about the Glasgowhaskellusers
mailing list