#11739: Simplify axioms; should be applied to types -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: 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 changed by goldfire: @@ -8,1 +8,1 @@ - But the example shows that the new expressiveness is not expressive + But this example shows that the new expressiveness is not expressive @@ -10,0 +10,23 @@ + + {{{ + 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 + }}} New description: 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! {{{ 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 }}} 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. 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. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11739#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11739: Simplify axioms; should be applied to types -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: 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 changed by goldfire: @@ -35,0 +35,5 @@ + + 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`. New description: 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. 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. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11739#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11739: Simplify axioms; should be applied to types -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 Resolution: | Keywords: 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 changed by simonpj: @@ -91,3 +91,3 @@ - but now (as you point out) the `ax[1]` is not necessarily OK. But I - hazard that the lack of the commuting isn't going to lose useful - optimisations. + 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. New description: 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. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11739#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler