Changes between Version 1 and Version 2 of NewAxioms/CoincidentOverlap

May 29, 2013 12:59:01 PM (4 years ago)



  • NewAxioms/CoincidentOverlap

    v1 v2  
    1414 * The current implementation retains the ability for coincident overlap among non-group instances, for backward compatibility (and because this case is not hard to implement).
    16  * The current implementation considers coincident overlap among equations within an instance group when matching. See the implementation notes [wiki:NewAxioms here] for more info.
     16 * The current implementation considers coincident overlap among equations within an instance group when matching. See below for more info.
    1818 * Coincident overlap (both between single instances and within an instance group) requires syntactic equality after expansion of vanilla type synonyms. In particular, type families are not expanded. Chak defends this design decision in the comments of #4259; that bug report is a request to lift this restriction. I ([ Richard]) think we should work to lift this restriction, taking Chak's points into consideration. For example, the following is tantalizing:
    20 type instance where
     20type instance Plus n m where
    2121  Plus Zero     n        = n
    2222  Plus (Succ m) n        = Succ (Plus m n)
    2626  Figuring out that the right-hand sides are confluent requires expanding the {{{Plus}}} type family one time. What do you think? Would this be useful?
     28== Coincident overlap within a branched instance ==
     30I (Richard) would like to be able to say this:
     33type family And (a :: Bool) (b :: Bool) :: Bool
     34type instance And a b where
     35  And False a     = False
     36  And True  b     = b
     37  And c     False = False
     38  And d     True  = d
     39  And e     e     = e
     42According to the [wiki:NewAxioms main page] about branched instances, "We only match a type against an equation in an instance group when no previous equation can unify against the type." Unfortunately, that kills us here. Consider reducing {{{And f True}}}. The first three branches clearly don't match. The fourth matches. But, the first two branches unify (i.e., they might apply later, depending on the instantiation for {{{f}}}), so we're stuck. Instead, we propose to scan through the branched instances at the declaration, and look to find only problematic orderings. In the declaration above, there are no problematic orderings -- if a previous branch might apply later, we'd get the same result anyway, so we're OK. Then, during matching, we only check problematic previous branches.
     44Another example is in order:
     47type instance F a where
     48  F Int  = Int
     49  F Bool = Char
     50  F a    = a
     53The only problematic ordering is {{{F Bool}}} before {{{F a}}}. Why? Let's consider this piece by piece. {{{F Int}}} can have no problematic previous branches, because it has no previous branches. A use site that matches {{{F Bool}}} will never later match {{{F Int}}}, {{{F Int}}} is not a problematic previous branch of {{{F Bool}}}. {{{F Int}}} might later match something that matches {{{F a}}}, but the right-hand sides coincide, so {{{F Int}}} is not problematic here either. On the other hand, {{{F Bool}}} might also later match something that matches {{{F a}}} and the right-hand sides ''don't'' coincide, so {{{F Bool}}} ''is'' problematic. The upshot is that, if {{{F a}}} matches a use site, we have to make sure that {{{F Bool}}} cannot later apply. Otherwise, we can skip that check.
     55This is perhaps somewhat subtle, but it seems to be the right way to do it.