Opened 3 years ago
Last modified 3 years ago
#4894 new feature request
Missing improvement for fun. deps.
Reported by: | diatchki | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | ⊥ |
Component: | Compiler (Type checker) | Version: | 7.1 |
Keywords: | Cc: | dimitris@…, mikhail.vorozhtsov@… | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Difficulty: | |
Test Case: | Blocked By: | ||
Blocking: | Related Tickets: |
Description
The problem is illustrated by the following example:
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} class F a b | a -> b f :: (F a b, F a c) => a -> b -> c f _ = id Results in the following error: Could not deduce (b ~ c) from the context (F a b, F a c) bound by the type signature for f :: (F a b, F a c) => a -> b -> c at bug.hs:6:1-8 `b' is a rigid type variable bound by the type signature for f :: (F a b, F a c) => a -> b -> c at bug.hs:6:1 `c' is a rigid type variable bound by the type signature for f :: (F a b, F a c) => a -> b -> c at bug.hs:6:1 Expected type: b -> c Actual type: b -> b In the expression: id In an equation for `f': f _ = id
The issue seems to be related to Note [When improvement happens] in module TcInteract?. It states that two "givens" do not interact for the purposes of improvement.
As far as I understand, the correct behavior should be to generate a new given equality, justified by the functional dependency on the class.
This is also related to bug #1241: in order to justify an improvement by functional dependency, we have to check that all instances are consistent with the dependency. Otherwise, the above function would turn into an "unsafe cast" function.
Change History (12)
comment:1 Changed 3 years ago by simonpj
- Cc dimitris@… added
comment:2 Changed 3 years ago by diatchki
I was thinking that each FD for a class, F, would correspond to a
built-in rule of the form:
ByFD F 0 :: (F a b, F a c) => (b ~ c) ... ByFD F n :: ...
and we'd use these rules to reason about FDs. The rules would work both
for givens (in which case they'd generate new facts), and for wanteds
(in which case they'd generate new goals). As far as I understand, there
would be no need for any special "improvement" code because everything
would be handled by the code for reasoning about equality. Furthermore,
we'd have a record of where FD-improvement kicked in, for sanity checking
purposes.
We ensure that the rule is valid by rejecting instances that might violate it.
This is essentially the same as checking that the instances of a type family
are consistent with each other, which is why we can conclude that
(B a ~ b, B a ~ c) => b ~ c.
comment:3 Changed 3 years ago by simonpj
But every "rule" should correspond to some evidence term in System FC. FC is our touchstone; it keeps us honest. Apart form anything else we have a type soundness theorem for it. Would you care to give an FC elaboration for your proposed program? (I can give one for the equality-superclass version.)
comment:4 Changed 3 years ago by diatchki
I was thinking that "ByFD" would be a new basic form of evidence in FC, defining what it means for a predicate to have a FD. As such, it has no proof in the system but it requires that when we extend the system by adding new instances, we check that they are consistent with the rules. The situation is analogous to the super-class check for an instance, and the consistency check for a type function.
I can see that we can also define what it means for a class to have a FD in terms of super-classes and type functions. This is probably OK, but I though I'd write down a few things which seem "a bit off" (not really problems but things we should watch out for):
- The encoding duplicates information because we have to provide definitions for both predicates (via class instances) and type functions (via type family instances), and the type instances are completely derived from the class ones. This makes programs larger, but also, it forces us to make some arbitrary choices, as illustrated by the following example:
instance (F a b, G a b) => C [a] b where ... -- F, G, and C all have a FD from the 1st argument to the 2nd.
Here, we can define the FD type function for C either in terms of F or G.
- The encoding introduces a dependency between language features which, conceptually, seem independent: it makes sense to have a language which has FDs on classes but no type functions, or even super-classes.
comment:5 Changed 3 years ago by simonpj
Well, if you are going to propose some new form of evidence in FC, it'd be good to be specific, and give the syntax, typing judgements, and operational semantics. A good starting point is the appendix of http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/. I don't yet understand the proposed extension.
Lacking such an extension, GHC's current position is to use fundeps for improvement, for 'wanted' constraints but not for 'given' ones. If you want to use the equalities for given ones, then use type functions.
I can believe that is sometimes infelicitous, but I didn't understand your example. Can you give an example where the type-function version is tiresome or annoying? Thanks.
comment:6 Changed 3 years ago by diatchki
(Thanks for the link, I've been looking at an older version of the paper).
I had forgotten that FC already had a built-in "axiom" construct. With this, I think that the only thing that would need to change is to generalize axioms to allow them to have parameters. This is a generalization because we can use it to express conditional equalities.
Then, what I was trying to say above amounts to: a class declaration with FDs
class C a b | a -> b, b -> a where ...
translates in FC to:
data C a b where ... axiom C_fd0 a b1 b2 : (C a b1, C a b2) => (b1 ~ b2) axiom C_fd1 a1 a2 b : (C a1 b, C a2 b) => (a1 ~ a2)
(I wrote the axiom parameters using "(...) =>" to mimic Hashell's notation)
comment:7 Changed 3 years ago by simonpj
No, that's not how axioms work in FC. They take the form
axiom C a b c : t1 ~ t2
where t1 and t2 are types, and a,b,c are the variables in which the axiom is parametric.
comment:8 Changed 3 years ago by diatchki
I understand that, I was saying that we might want to generalize how axioms work in FC.
I realize that this ticket is probably not the right place to do this so, if I can find some time, I'll try to write up what I was thinking in a separate e-mail. This would probably be useful for my work on the type nats too, the outcome being that I'd either find out that I was confused about something, or perhaps, we could generalize FC a bit.
comment:9 Changed 3 years ago by simonpj
Ah yes. Generalising FC might be good. By all means propose such a thing.
comment:10 Changed 3 years ago by igloo
- Milestone set to 7.2.1
comment:11 Changed 3 years ago by simonpj
- Milestone changed from 7.2.1 to _|_
- Type changed from bug to feature request
Actually this is more of a feature request than a bug, and depends on some as-yet-undeveloped theory.
Simon
comment:12 Changed 3 years ago by mikhail.vorozhtsov
- Cc mikhail.vorozhtsov@… added
No, GHC has no way to do this. Not because of shortcomings in the inference engine, but because the FC language can't express it. The question is this: where is the *evidence* that (b~c). Alas there isn't any.
This is a place where the "encoding" of fundeps using type functions actually works better:
Now if you have given constraints (ie evidence for) F a b, F a c), then you also have evidence for b ~ B a, c ~ B a, and hence by transitivity for b~c.
Fundeps in GHC are handled just as in Hugs, as "improvement rules" only, meaning that they narrow the search space by suggesting unifications. But they don't provide evidence.
Having equalities as superclasses isn't working properly yet, but it's my current priority.
Does this make sense?
Simon