Changes between Version 4 and Version 5 of NewAxioms/CoincidentOverlap


Ignore:
Timestamp:
Aug 23, 2013 7:39:00 PM (23 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/CoincidentOverlap

    v4 v5  
    1 = Overlapping Type Family Instances with Coincident Right-Hand Sides = 
     1= Closed Type Families with Coincident Right-Hand Sides = 
    22 
    3 In the official release of GHC, it is permitted to write something like this: 
     3In GHC 7.6, it is permitted to write something like this: 
    44 
    55{{{ 
     
    1010These instances surely overlap, but in the case when they do, the right-hand sides coincide. This page explores the design space around this feature with an eye toward adding instance groups, as discussed [wiki:NewAxioms here]. 
    1111 
    12  * In the current (Aug 2012) implementation of family instance groups, no overlap (even coincident) overlap is allowed between a group and another instance. It may be possible to change the implementation to allow such overlap, but it adds another layer of complexity to the GHC code and may not be worth it. Add comments if you have a good use case for why we need coincident overlap involving an instance group. 
    13  
    14  * 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). 
    15  
    16  * The current implementation considers coincident overlap among equations within an instance group when matching. See below for more info. 
    17  
    18  * 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 ([http://www.cis.upenn.edu/~eir Richard]) think we should work to lift this restriction, taking Chak's points into consideration. For example, the following is tantalizing: 
    19 {{{ 
    20 type instance Plus n m where 
    21   Plus Zero     n        = n 
    22   Plus (Succ m) n        = Succ (Plus m n) 
    23   Plus m        Zero     = m 
    24   Plus m        (Succ n) = Succ (Plus m n) 
    25 }}} 
    26   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? 
    27  
    28 == Coincident overlap within a branched instance == 
     12== Coincident overlap within a closed type family == 
    2913 
    3014This section discusses a part of the "Concrete Proposal" on [wiki:NewAxioms/Nonlinearity this page] to patch a potential hole in Haskell's type system. 
     
    3317 
    3418{{{ 
    35 type family And (a :: Bool) (b :: Bool) :: Bool 
    36 type instance And a b where 
     19type family And (a :: Bool) (b :: Bool) :: Bool where 
    3720  And False a     = False 
    3821  And True  b     = b 
     
    4225}}} 
    4326 
    44 According 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. 
     27According to the [wiki:NewAxioms main page] about closed type families, "We only match a type against an equation in a closed type family 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 scan through the equations at the declaration and look to find compatible equations. Two equations are compatible if their right-hand sides match whenever their left-hand sides do. In the declaration above, all equations are compatible -- if a previous equation might apply later, we'd get the same result anyway, so we're OK. Then, during matching, we only check ''in''compatible previous equations. 
    4528 
    4629Another example is in order: 
    4730 
    4831{{{ 
    49 type instance F a where 
     32type family F a where 
    5033  F Int  = Int 
    5134  F Bool = Char 
     
    5336}}} 
    5437 
    55 The 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. 
     38The only incompatible pair of equations is {{{F Bool}}} and {{{F a}}}. Why? Let's consider this piece by piece. A use site that matches {{{F Bool}}} will never later match {{{F Int}}}, so {{{F Int}}} is compatible with {{{F Bool}}}. {{{F Int}}} might later match something that matches {{{F a}}}, but the right-hand sides coincide, so these equations are compatible. On the other hand, {{{F Bool}}} might also later match something that matches {{{F a}}} and the right-hand sides ''don't'' coincide, so these equations are not compatible. 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. 
    5639 
    5740This is perhaps somewhat subtle, but it seems to be the right way to do it. 
     
    5942The ideas discussed here stem from posts by AntC, Andy Adams-Moran, and Richard on Richard's [http://typesandkinds.wordpress.com/2013/04/29/coincident-overlap-in-type-families/ blog post] on the subject. 
    6043 
    61 == Cross-module coincident overlap (or lack thereof) == 
    62  
    63 [wiki:NewAxioms/Nonlinearity This proposal] has the net effect of forcing all uses of coincident overlap to appear in one module, instead of spread across modules. That's admittedly not great, but it's possible that no one will be negatively affected. The only alternative we've (Simon, Dimitrios, Richard) thought of is to disallow coincident overlap when the left-hand sides are non-linear, but that seems very ugly and ad-hoc.