Hello, On Wed, Jun 15, 2011 at 12:25 AM, Simon Peyton-Jones wrote:

| > class C a b | a -> b where | > foo :: a -> b | > foo = error "Yo dawg." | > | > instance C a b where | | The instance 'C a b' blatantly violates functional dependency and | should not have been accepted. The fact that it was is a known bug in | GHC. The bug keeps getting mentioned on Haskell mailing lists | about every year. Alas, it is still not fixed. Here is one of the | earlier messages about it: | | http://www.haskell.org/pipermail/haskell-cafe/2007-March/023916.html

Wait. What about instance C [a] [b] ? Should that be accepted? The Coverage Condition says "no", and indeed it is rejected. But if you add -XUndecidableInstances it is accepted.

It's just the same for instance C a b It is rejected, with the same message, unless you add -XUndecidableInstances.

Do you think the two are different? Do you argue for unconditional rejection of everything not satisfying the Coverage Condition, regardless of flags?

No, those two are not different, the instance "C [a] [b]" should also be rejected because it violates the functional dependency. The fact that -XUndecidableInstances accepts this is exactly the bug that keeps being mentioned on the lists every now and then. The reason that this instance violates the functional dependency is that it allows us to conclude both "C [Int] [Bool]", and "C [Int] [Char]", and clearly "[Int] = [Int]", but "[Bool] /= [Char]". The general rule defining an FD on a class like "C" is the following logical statement: "forall a b1 b2. (C a b1, C a b2) => (b1 = b2)" (So I think that the basic concept is really very simple and precise. I agree that the implementation can be tricky, but a lot of the difficulties are shared with type families---we are just dealing with a hard problem.) With simple instances (no contexts) it is easy to check if a set of instances is consistent with the FDs of the classes, however when we have conditional instance the task is harder. This is why we have approximations that ensure consistency (e.g., the Coverage Condition). My understanding is that the coverage condition in GHC ensures both consistency with the FDs, and termination of the process. In the past we had another condition, which ensured consistency but not necessarily termination (I forget its name now but, basically, the rule said that all variables in the target of an FD should be determined from the variables in the source of the FD, but we can use FDs in the context of the instance). I think the GHC bug is that with -XUndecidableInstances, instances are not validated at all wrt to FDs. A way to fix that would be to switch to using the old FD validation rule when -XUndecidableInstances are turned on. -Iavor Simon

_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime

Hello, On Wed, Jun 15, 2011 at 10:49 AM, wrote:

At Wed, 15 Jun 2011 10:10:14 -0700, Iavor Diatchki wrote:

...

Hello,

On Wed, Jun 15, 2011 at 12:25 AM, Simon Peyton-Jones <

simonpj@microsoft.com>

...

wrote:

| > class C a b | a -> b where | > foo :: a -> b | > foo = error "Yo dawg." | > | > instance C a b where

Wait. What about instance C [a] [b]

No, those two are not different, the instance "C [a] [b]" should also be rejected because it violates the functional dependency.

But now you are going to end up rejecting programs like this:

{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-}

class C a b | a -> b class D a b | a -> b instance (D a b) => C [a] [b]

And a lot of useful code (including HList) depends on being able to do things like the above.

Nope, this program will not be rejected because "b" is in the FD closure of "a". This stuff used to work a few GHC releases back, and I think that this is the algorithm used by Hugs. A functional dependency on a class imposes a constraint on the valid class instances (in a similar fashion to adding super-class constraints to a class). In general, checking this invariant may be hard, so it is fine for implementations to be "incomplete" (i.e., reject some programs that do satisfy the invariant or, perhaps, fail to terminate in the process). OTOH, I think that if an implementation accepts a program that violates the invariant, then this is a bug in the implementation.

...

The general rule defining an FD on a class like "C" is the following logical statement: "forall a b1 b2. (C a b1, C a b2) => (b1 = b2)"

And in fact b1 and b2 are equal, up to alpha-conversion. They are both just free type variables.

No, this was intended to be a more "semantic" property. Here it is in English: For any three ground types "a", "b1", and "b2", if we can prove that both "C a b1" and "C a b2" hold, then "b1" and "b2" must be the same type. The theory of functional dependencies comes from databases. In that context, a class corresponds to the schema for a database table (i.e., what columns there are, and with what types). An instance corresponds to a rule that adds row(s) to the table. With this in mind, the rule that I wrote above exactly corresponds to the notion of a functional dependency on a database table. -Iavor

First of all, I do agree with David. Overlapping instances are indeed very useful in practice, cutting down significant amount of boiler-plate. His examples, as well the example from polymorphic map libraries (mentioned earlier) are real-world cases where overlapping instances are invaluable and indispensable. I do wish to point out the need for `proper credit': is the benefit specifically because of overlapping, or functional dependencies alone suffice? As far as I noticed, all compelling examples used and relied on overlapping instances (not just functional dependencies or undecidable instances) The functional dependencies per se are quite well understood: see The theory of overloading Peter J. Stuckey and Martin Sulzmann TOPLAS, 2005, v27, N6, 1216--1269 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.837 (perhaps there is a better URL, to the final version of the paper) Language and Program Design for Functional Dependencies Mark P. Jones, Iavor S. Diatchki http://web.cecs.pdx.edu/~mpj/pubs/fundeps-design.html `The theory of overloading' should answer Dan Doel's question about the ideal way of handling functional dependencies. The paper should also answer all of David's questions about functional dependencies, explaining why Iavor and I so object to class C a b | a -> b instance C a b It is the overlapping instances that muddy the water (especially in combination with other Haskell features such as higher-rank types). There is a nagging feeling that the combination may even be unsound. But the overlapping instances are so useful and compelling! That is exactly the problem that started this thread, as I understand. I do wish to stress the solution I have proposed earlier. I think it helps implement all of David's examples (and all of mine examples), without overlapping instances. Whether one uses functional dependencies or type functions is a secondary, and minor issue. The solution could be implemented (in ugly way) even now, but will benefit from _small_ GHC support. There are NO changes to GHC core or to the FC calculus are required. David wrote:

class C a b | a -> b where aDefault :: a aTobC :: a -> b class D a b where -- no fundep aTobD :: a -> b instance (D Int b) => C Int b where -- should this be allowed? aDefault = 0 aTobC = aTobD

class C' a b | a -> b class E a b | a -> b -- unlike above, we now have a fundep instance (E a b) => C' a b

Oleg, you haven't weighed in this specific question, but I think many of your ideas require the ability to write instances like C', even if you advocate disallowing C.

I would argue for rejection of the instance of C but accepting C'. The Prolog program posted yesterday will back me up. I should stress the underlying reason. First of all, when considering if an instance violates functional dependency, the methods of the instance are irrelevant. Only the instance head and its constraints matter. Here is why. Recall the main property: (C a b1, C a b2) ==> b1 ~ b2 Here is the corollary: given instance C Int Bool and the type forall t. C Int t => t we _improve_ the type to just Bool. The type equality constraint t ~ Int lets us replace all occurrences of the variable t with Int. This is exactly the sort of substitution that underlies lambda-calculus. Thus, the process of improvement simulates general computation. Thus functional dependencies let us write and run type-level programs.

Okay, we seem to be having a debate where, to caricature only a little, I'm arguing that Fundeps/UndecidableInstances are ugly but useful, and other people are arguing that they are truly absolutely horrible in their current GHC implementation. I think the debate boils down to where you see the scope of the implicit universal quantification of free type variables in instances. Consider the following: class C a b | a -> b where aDefault :: a aTobC :: a -> b class D a b where -- no fundep aTobD :: a -> b instance (D Int b) => C Int b where -- should this be allowed? aDefault = 0 aTobC = aTobD GHC accepts this above code, which makes sense to me because I read the instance declaration as essentially (in pseudo-Haskell): forall b. instance (D Int b) => C Int b or, equivalently: instance C Int (forall b. (D Int b) => b) In English, "there's only one instance of C with (a ~ Int), but, in that instance, the aTobC method returns a value of type b for any b you want, except that in order to produce the value, it needs access to an appropriate dictionary of class D." One corollary of this view is that it is impossible to violate functional dependencies without defining more than one instance of a class. The alternate reading (and please correct me if I'm mis-characterizing the argument), is that we should apply the functional dependencies of a class to each individual instance, where any universal quantification happens across the fundep. According to this view, we should read C's instance declaration as: forall b. (instance (D Int b) => C Int b | Int -> b) and find that "forall b. ... | Int -> b" fails. Hence, we have violated functional dependencies with a single instance of the class. There's a less explicit but equally important question underlying this discussion about how much contexts should play into instance validation. Some have suggested GHC should reject the above instance of C, but should nonetheless accept the following instance of C': class C' a b | a -> b class E a b | a -> b -- unlike above, we now have a fundep instance (E a b) => C' a b Oleg, you haven't weighed in this specific question, but I think many of your ideas require the ability to write instances like C', even if you advocate disallowing C. On this question, I am opposed, because I find it too reminiscent of an aspect of C++ I dislike, namely that ad-hoc polymorphism interacts with templates, implicit promotion, and the most-specific match rule to make it hard to understand code. (And since, unlike C++, Haskell allows polymorphic return types, there's a potential for things to get even more complicated.) Fortunately, GHC's current approach is quite simple: The instance head is always sufficient to determine whether or not an instance matches, two instances overlap, or functional dependencies are violated. The context may tell you what dictionaries must be around if you actually want to use an instance, but if you know that a program compiles, you can ignore the context when reading and reasoning about the code. Another reason that I oppose too much reliance on the context is that I want the ability to load code dynamically. If the assumption about ground type equality is pushed too far--e.g., allowing coercion based on reasoning about fundeps--then dynamically loading modules with contradictory fundeps could undermine memory safety. One of my objections to type families is the difficulty of guaranteeing safety in the presence of dynamic loading. At any rate, this is the haskell-prime mailing list, not the how-much-do-you-hate-some-current-ghc-option-implementation list. I've already taken a lot of people's time with this thread, so let me propose to do something useful for the haskell prime effort. I could start a compilation (probably a wiki page) of things you can do or might want to do with fundeps and undecidable/overlapping instances. This could serve as a kind of wish list for Haskell prime. Examples off the top of my head might be: - Type-safe dynamic loading - Sqrt(N) reduction in code size for mtl instances - HList/OO-Haskell - Enforcing simple recursively-defined properties on types. (E.g., with GHC 7.2's new generic deriving framework, you might want to specify the constraint that a type's Representation doesn't include NoSelector.) - Using data types to represent ad-hoc polymorphic functions you can pass as arguments to functions. E.g., using a class like: class Function f a b | f a -> b where funcall :: f -> a -> b you can define types f of class Function and use them to do maps over tuples. Someone thinking of implementing an idea (e.g., closed type families) could look at the wish list and determine out how much of it the new feature would cover. Others could add to the wish list. Oleg, I realize the list might resemble your bibliography, but the idea would be to list the simplest possible cases (like C' above), rather than examples that unleash the full power of the extension. We can link to your web site for people who want to delve deeper into the motivation. If that sounds like a useful idea, the next question is where to put such a list. The Haskell prime wiki seems like a logical place, but it should be someplace where multiple people can edit it. (And, though I have an account on the Haskell prime wiki, username David, I can't seem to edit stuff there.) David