Opened 3 years ago
Last modified 3 years ago
#11739 new task
Simplify axioms; should be applied to types
Reported by: | goldfire | Owned by: | goldfire |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.1 |
Keywords: | Cc: | ||
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description (last modified by )
Simon PJ says:
In Note [Coercion axioms applied to coercions]
in Coercion, we find the justification for allowing coercions as arguments to axioms. The goal is to add a bit of extra expressiveness, so that optimisations can be done pair-wise.
But this example shows that the new expressiveness is not expressive enough, given the apartness restrictions on closed type families. (The goal is to eliminate the call to checkAxInstCo
in OptCoercion.)
type family F (a :: *) (b :: *) where F a a = Int F a b = b type family Id (a :: *) where Id a = a ---------------------- axF :: { [a::*]. F a a ~ Int ; [a::*, b::*]. F a b ~ b } axId :: [a::*]. Id a ~ a co1 = axF[1] (axId[0] <Int>) (axId[0] <Bool>) :: F (Id Int) (Id Bool) ~ Bool co2 = sym (axId[0] <Bool>) :: Bool ~ Id Bool co3 = co1 ; co2 :: F (Id Int) (Id Bool) ~ Id Bool co3' = optimized co3 = axF[1] (axId[0] <Int>) <Id Bool> -- bogus, fails call to checkAxInstCo
This last co3'
is what would be produced if we didn't run checkAxInstCo
. But, as the comment says, it runs afoul of the apartness condition (as checked by checkAxInstCo
). Currently, OptCoercion just gives up in this case, retaining the original co3
.
Rather than give up (as you do in OptCoercion) maybe we should re-examine the assumption. How could we optimise if axioms could only be instantiated with types, not coercions. Which would be a LOT simpler!
Let's take the example from the Note:
C a : t[a] ~ F a g : b ~ c
and we want to optimize
sym (C b) ; t[g] ; C c :: F b ~ F c
One possibility is to perform a 3-component optimisation, but that's a bit horrible. But what about this: push the t[g]
past the axiom rather than into it. For example
t[g] ; C c ==> C b ; F g where t[g] : t[b]~t[c] C c : t[c] ~ F c
If we use this to move axioms to the right, I think we'll get the same optimisations as now, but with a simpler system. Does that seem right?
Now it becomes clearer that you can't always commute the things.
ax : F a a ~ a; F a b ~ b co :: Id Bool ~ Bool
If we have
(F <Int> co ; ax[1] Int Bool) : F Int (Id Bool) ~ Bool
then we might try to commute co
past the axiom thus:
ax[1] Int (Id Bool) ; co
but now (as you point out) the ax[1]
is not necessarily OK; so we still need to use checkAxInstCo
. But I hazard that the lack of the commuting isn't going to lose useful optimisations.
So in some ways we are no further forward (an optimisation is only sometimes OK), but I feel MUCH happier about simplifying the axiom-applied-to-coercion stuff.
Change History (6)
comment:1 Changed 3 years ago by
Description: | modified (diff) |
---|
comment:2 Changed 3 years ago by
Description: | modified (diff) |
---|
comment:3 Changed 3 years ago by
Description: | modified (diff) |
---|
comment:4 Changed 3 years ago by
Description: | modified (diff) |
---|
comment:5 Changed 3 years ago by
Description: | modified (diff) |
---|
comment:6 Changed 3 years ago by
Owner: | set to goldfire |
---|