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 simonpj)

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
    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 goldfire

Description: modified (diff)

comment:2 Changed 3 years ago by goldfire

Description: modified (diff)

comment:3 Changed 3 years ago by goldfire

Description: modified (diff)

comment:4 Changed 3 years ago by simonpj

Description: modified (diff)

comment:5 Changed 3 years ago by simonpj

Description: modified (diff)

comment:6 Changed 3 years ago by goldfire

Owner: set to goldfire
Note: See TracTickets for help on using tickets.