Why only inference in type checking?
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.
| 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. Actually GHC's type check uses checking when it knows the types, and inference only when it doesn't. | 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? It exactly does meet-in-the-middle. Maybe you can elaborate your reasoning? In any case, the restrictions on fundeps are needed for checking too. I believe. Simon
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
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@utwente.nl] | Sent: 19 October 2007 09:38 | To: Simon Peyton-Jones | Cc: glasgow-haskell-users@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
participants (2)
-
Philip K.F. Hölzenspies -
Simon Peyton-Jones