RE: Problem with functional dependencies
I think you can simplify the example. Given class HasFoo a b | a -> b where foo :: a -> b instance HasFoo Int Bool where ... Is this legal? f :: HasFoo Int b => Int -> b f x = foo x You might think so, since HasFoo Int b => Int -> b is a substitution instance of HasFoo a b => a -> b but if we infer the type (HasFoo Int b => Int -> b) for f's RHS, we can then "improve" it using the instance decl to (HasFoo Int Bool => Int -> Bool), and now the signature isn't a substitution insance of the type of the RHS. Indeed, this is just what will happen if you try with GHC, because GHC takes advantage of type signatures when typechecking a function defn, rather than first typechecking the defn and only then comparing with the signature. I don't know what the answers are here, but there's more to this functional dependency stuff than meets the eye. Even whether one type is more general than another has changed! Simon | -----Original Message----- | From: qrczak@knm.org.pl [mailto:qrczak@knm.org.pl] | Sent: 17 December 2000 19:30 | To: haskell@haskell.org | Subject: Problem with functional dependencies | | | The following module is rejected by both | ghc -fglasgow-exts -fallow-undecidable-instances | and | hugs -98 | | -------------------------------------------------------------- | ---------- | class HasFoo a foo | a -> foo where | foo :: a -> foo | | data A = A Int | data B = B A | | instance HasFoo A Int where | foo (A x) = x | | instance HasFoo A foo => HasFoo B foo where | foo (B a) = foo a | -------------------------------------------------------------- | ---------- | | The error messsage says that the type inferred for foo in B's instance | is not general enough: the rhs has type "HasFoo B Int => B -> | Int", but | "HasFoo B foo => B -> foo" was expected.
Simon Peyton-Jones wrote:
I think you can simplify the example. Given
class HasFoo a b | a -> b where foo :: a -> b
instance HasFoo Int Bool where ...
Is this legal?
f :: HasFoo Int b => Int -> b f x = foo x
You might think so, since HasFoo Int b => Int -> b is a substitution instance of HasFoo a b => a -> b
This is the step where the reasoning goes wrong. The functional dependency tells you that `b' isn't really a free variable, since it is dependent on `a'. If you substitute for `a', you can't expect `b' to remain unconstrained. Hugs complains that the inferred type for `f' is not general enough. It's right to complain, but the real problem is that the signature is too general. Asimilar situation arises if you try to declare an instance `HasFoo Int b', but in this case, hugs complains that the instance is more general than the dependency allows. A useful thing to do would be to check for this sort of thing in signatures as well, so that the more appropriate error message can be given. --Jeff
Thu, 21 Dec 2000 00:59:29 -0800, Jeffrey R. Lewis <jeff@galconn.com> pisze:
class HasFoo a b | a -> b where
f :: HasFoo Int b => Int -> b f x = foo x
This is the step where the reasoning goes wrong. The functional dependency tells you that `b' isn't really a free variable, since it is dependent on `a'. If you substitute for `a', you can't expect `b' to remain unconstrained.
It's not unconstrained: the constraint is "HasFoo Int b", as written. IMHO it should not matter that the constraint fully determines b.
Asimilar situation arises if you try to declare an instance `HasFoo Int b', but in this case, hugs complains that the instance is more general than the dependency allows.
ghc does not complain. How would I express "the instance can be chosen basing on 'a' alone, and the instance found will tell what constraints are on 'b'"? Aren't fundeps a too general mechanism which is not able to express simpler statements? :-( -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
Simon Peyton-Jones wrote:
I think you can simplify the example. Given
class HasFoo a b | a -> b where foo :: a -> b
instance HasFoo Int Bool where ...
Is this legal?
f :: HasFoo Int b => Int -> b f x = foo x
You might think so, since HasFoo Int b => Int -> b is a substitution instance of HasFoo a b => a -> b
but if we infer the type (HasFoo Int b => Int -> b) for f's RHS, we can then "improve" it using the instance decl to (HasFoo Int Bool => Int -> Bool), and now the signature isn't a substitution insance of the type of the RHS.
I definitely want it to be legal. I have examples where this is immensly useful. -- -- Lennart
| I think you can simplify the example. Given | | class HasFoo a b | a -> b where | foo :: a -> b | instance HasFoo Int Bool where ... | | Is this legal? | f :: HasFoo Int b => Int -> b | f x = foo x The theoretical foundation for functional dependencies goes back to the work I did on "Simplifying and Improving Qualified Types". (Interested parties can find a 1994 report on this on my web pages; email me if you need a pointer.) According to that theory, the type above is a "principal satisfiable type" for f, as is the more accurate Int -> Bool: under the satisfiability ordering described in the report, these two types are (satisfiably) equivalent. There is, therefore, no technical reason why the function f could not be treated as having the polymorphic type shown above. On the other hand, from a practical perspective, one can argue that the polymorphic type is misleading, obfuscating, and cumbersome: Misleading because f doesn't really have a polymorphic type as the declaration pretends; Obfuscating because it forces a reader to study instance declarations that are not included in the type; and Cumbersome because it includes an unnecessary (HasFoo Int b) constraint that could be eliminated to produce a shorter, simpler type. So it comes down to a language design *decision* for which functional dependencies, by themselves, do not force a particular choice. - The current Hugs implementation does not allow the polymorphic type; the intention in that implementation was to infer more accurate, less complex types. The idea here is to make programs easier for programmers to read, write, and understand. - Marcin indicates that he would prefer the more relaxed approach that allows polymorphic types; he is writing a preprocessor that generates type signatures, and his task is easier if he doesn't have to worry about the "improvement" of class constraints. The idea here is to make programs easier for generators to read, write and manipulate. Clearly, some compromise is needed because neither approach is right for all purposes. If we look to other aspects of the language for inspiration, then the best way to deal with this is (probably): (i) to infer simpler types whenever possible, but (ii) to allow more polymorphic types when they are requested by means of an explicit type signature. (Incidentally, in the interests of consistency, such a system should also programmers to use types like Num Int => Int -> Bool.) All the best, Mark
On 03-Jan-2001, Mark P Jones <mpj@cse.ogi.edu> wrote:
... the best way to deal with this is (probably): (i) to infer simpler types whenever possible, but (ii) to allow more polymorphic types when they are requested by means of an explicit type signature.
I agree.
(Incidentally, in the interests of consistency, such a system should also programmers to use types like Num Int => Int -> Bool.)
Mercury uses the approach you've suggested above for constraints like these. That is, you can declare types like that, and the Mercury type checker will accept them, but it won't try to infer such types. This feature could be a bit more useful in Mercury than in Haskell, since in Mercury instance declarations can be private to a particular module. (Unfortunately, though, the Mercury runtime system's RTTI representation of instances is not able to handle such constraints, so for such examples, the current implementation of the compiler reports "sorry, not implemented: constraints may only constrain type variables".) -- Fergus Henderson <fjh@cs.mu.oz.au> | "I have always known that the pursuit | of excellence is a lethal habit" WWW: <http://www.cs.mu.oz.au/~fjh> | -- the last words of T. S. Garp.
I don't fully understand fundeps. Would the following transform legal programs (without overlapping instances) into legal programs? I hope yes. Let's imagine a class with a set of instances and uses, without fundeps. - Add some additional type variables to the class header. - Add a fundep: all old type variables -> all new type variables. - For each instance, in places corresponding to new type variables write arbitrary types. - For each constraint based on this class, in places corresponding to new type variables write unique type variables. In particular, should the following be legal: class C a b c | a -> b c instance C [a] b b f:: C [a] b c => a f = undefined ghc panics and Hugs rejects it. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
Hi Marcin, | In particular, should the following be legal: | | class C a b c | a -> b c | instance C [a] b b | f:: C [a] b c => a | f = undefined | | ghc panics and Hugs rejects it. No, it is not legal. Even if you delete the definition of f, the code is still not legal because the class and the instance declaration are inconsistent. The class declaration says that you want to define a three place relation on types called C. We can think of the entries in this relation as rows in a table with columns headed a, b, and c: a | b | c C = -----+-----+------ | | Before we take a look at any instance declarations, this table is empty (i.e., there are no rows). But the functional dependency a -> b c that you have specified establishes a constraint that any data that gets added to the table by subsequent instance declarations must satisfy. It says that, if two rows have the same type in the a column, then they must also have the same types in the b and c columns; "the values of b and c are uniquely determined by the value of a." So here are two plausible instance declarations that you could use: instance C Int Int Char instance C (Maybe t) t Int Notice that the second declaration here is really an instance scheme; the presence of a variable "t" means that it introduces a whole family of instances, one for each possible instantiation of the variable "t". With these two instance declarations in hand, our table looks something like the following: a | b | c C = ------------------+-----------+------ Int | Int | Char Maybe Int | Int | Int Maybe Bool | Bool | Int Maybe Char | Char | Int Maybe [Int] | [Int] | Int Maybe (Maybe Int) | Maybe Int | Int ... | ... | ... Conceptually, of course, there are now infinitely many rows in the table, so what you see here is just a small part of the relation. But notice that the data in the table is entirely consistent with the functional dependency a -> b c because no two rows have the same type in the a column. Now consider the instance declaration that you have given: instance C [t] s s Again, this is an instance scheme, generating one row in the table for each possible instantiation of variables "t" and "s". (To avoid confusion with the names of the columns in C, I've chosen different variable names from the ones you've used.) For example, based on this instance declaration, we would expect to continue adding rows to the table along the following lines: a | b | c C = ------------+-------+------- [Int] | Int | Int t=Int, s=Int [Int] | Bool | Bool t=Int, s=Bool [Bool] | Int | Int t=Bool, s=Int ... | ... | ... I hope now that the problem is becoming clear: this instance declaration is not consistent with the dependency; in the first two lines above, for example, we see two rows that violate the specification because they have the same value of "a", but different values for "b" and "c". In summary, the class declaration and its associated dependency are not consistent with the instance declaration. If you really wanted the rows described by the instance declaration to be part of the relation C, then the dependency you have written is not valid. If you really did want the restriction captured by the dependency, then the instance declaration is not valid. Hugs can't tell which of these is the real source of the problem, but it does report, correctly, that there is an inconsistency. A little more generally, given the class declaration and the dependency that you've specified, Hugs will not allow any instance declaration for something of the form C t1 t2 t3 if there are variables in t2 or t3 that do not appear in t1. If this restriction were not enforced, then it would again be possible for there to be multiple rows with the same "a" value, but different "b" and "c" entries. I noticed the same problem in one of the earlier examples that you sent to the list: | class Foo a b | a | instance Foo Int [a] | -- This is rejected by Hugs (with fundep a->b) but I would definitely | -- accept it. I hope that it is now clear why Hugs rejects this definition. | I don't fully understand fundeps. The specific point described above is actually discussed twice in my ESOP paper, once informally, and once in a more general setting. I encourage you to take a look at that paper for more details. If you're basing your knowledge of fundeps on the (now quite outdated) note on my web page, or on the section of the Hugs manual on which it was based, you may well have some gaps to fill in. I'm not too happy with the ESOP paper either; I couldn't include as much technical material there as I wanted because of limited space. If you have read the ESOP paper and still have questions, please let me know and I will do my best to answer them. All the best, Mark
Thu, 4 Jan 2001 13:01:56 -0800, Mark P Jones <mpj@cse.ogi.edu> pisze:
I hope now that the problem is becoming clear: this instance declaration is not consistent with the dependency; in the first two lines above, for example, we see two rows that violate the specification because they have the same value of "a", but different values for "b" and "c".
I see. So fundeps are not capable of expressing what I hoped, and what a related but simpler concept I talked about once can express. I wonder if there are practical uses of fundeps which are not expressible by this concept. What I have in mind is the following. A subset of type variables of a class is chosen. Only that subset is used to find an instance for resolving constraints with this class. The instance chosen determines the rest of types. Instances must make this possible, i.e. be non-unifiable wrt. the active subset of type variables. Voila. An extended variant: several such subsets instead of one. Probably each subset should be considered independently, with their results unified. Or something like that. This provides an equivalent of types contained in classes in C++. It does not matter if the passive types in an instance use additional type variables. This is where fundeps fail. Having types with type variables which are never instantiated nor constrained should be equivalent to having ground types! Why, oh why haven't a more friendly and less problematic concept been used, instead of fundeps which forever can't be finished in ghc and have some different semantics in Hugs? -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
participants (6)
-
Fergus Henderson -
Jeffrey R. Lewis -
Lennart Augustsson -
Mark P Jones -
qrczak＠knm.org.pl -
Simon Peyton-Jones