Changes between Version 25 and Version 26 of NewAxioms/Nonlinearity


Ignore:
Timestamp:
May 30, 2013 8:13:53 PM (11 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/Nonlinearity

    v25 v26  
    2626== General idea for the solution == 
    2727 
    28 We need to consider the two instances of {{{F}}} to be overlapping and inadmissible. There are a handful of ways to do this, but the best seems to be this:  
     28We need to consider the two instances of {{{F}}} to be overlapping and inadmissible. There are a handful of ways to do this: 
    2929 * (A) '''when performing the overlap check between two instances, check a version of the instances where all variables are distinct''' 
    3030We call the "version of the instance where all variables are distinct" the "linearized form" of the instance. 
     
    3636 
    3737Conor's alternative general idea: 
    38  * (B) '''when performing the overlap check, during unification succeed (instead of failing) if the occurs check happens''' 
    39 Remember "unification succeeds" means "overlap detected", so (B) is a bit more permissive than (A).  For example 
     38 * (B) '''when performing the overlap check, allow two types to overlap even if only infinite types would witness the overlap''' 
     39The idea here is that our root problem comes from a combination of nonlinearity and infinite types. So, simply make the overlap checker consider the possibility of types that contain themselves (the only possible form of infinite types). 
     40(B) is a bit more permissive than (A).  For example 
    4041{{{ 
    4142  type instance Good x   x    = blah 
    4243  type instance Good Int Bool = boo 
    4344}}} 
    44 These would be considered overlapping by (A), but accepted as non-overlapping (ie unification fails) by (B).  And indeed these two are fine (ie cannot give rise to unsoundness). 
     45These would be considered overlapping by (A), but accepted as non-overlapping by (B).  And indeed these two are fine (ie cannot give rise to unsoundness). 
    4546 
    46 Intuition: under (B) the only way that unification fails is because of a definite conflict (eg `Int` ~ `Bool`).  And unification failing is what allows us to accept the two equations as non-overlapping.  So if we accept them, they have a definite conflict. 
     47Intuition: under (B) the only way that two types don't overlap is because of a definite conflict (eg `Int` ~ `Bool`).  
     48 
     49How to implement (B)? It may be as easy as omitting the occurs check during unification. The way GHC detects overlap is by trying to unify the left-hand sides of two instances. If they can unify, then they overlap. Currently (GHC 7.6.3), unification fails for the two instances for `F` above, so they don't overlap. The unification fails because of the so-called "occurs check": when we are unifying a type variable (say, `x`) against a non-type-variable, (say `[x]`), we check to make sure that the type variable does not appear anywhere within the non-type-variable. (If the variable does appear in the other type, then the substitution has no fixpoint.) We could simply turn this check off, in this particular case. The net effect is to consider the possibility of infinite types. 
     50 
     51But, it just might not be so easy. What, exactly, should the unification algorithm do when the occurs check notes an occurrence in this case? Normally, the algorithm builds a substitution, but that would be impossible here. Yet, we need to record ''something'' about what we've discovered. For example, take this: 
     52 
     53{{{ 
     54type family NotSure x y 
     55type instance NotSure x x = Int 
     56type instance NotSure [x] (Maybe x) = Bool 
     57}}} 
     58 
     59It seems that these do not overlap, even in the presence of infinite types. But, a naive omission of the occurs check might say that these types do overlap. Getting this case wrong isn't terrible, but it would be nice to get it right. (Note that we would end up too conservative, which is OK in this case.) 
    4760 
    4861== Problem: coincident overlap ==  
     
    5770These instances surely overlap, but in the case when they do, the right-hand sides coincide. We call this '''coincident overlap'''. 
    5871 
    59 However, the above proposal of linearizing the LHS before checking overlap makes a nonsense of exploiting coincident overlap, because when we freshen the LHS we no longer bind the variables in the RHS. '''So the proposal abandons support for coincident overlap between standalone type instances'''.  (It's worth noting, though, that there is already no support for coincident overlap between branched type instances, or between a singleton type instance and a branched one; it is currently only supported between singleton type instances.) 
     72However, the above proposal of linearizing the LHS before checking overlap (plan (A)) makes a nonsense of exploiting coincident overlap, because when we freshen the LHS we no longer bind the variables in the RHS. '''So the proposal abandons support for coincident overlap between standalone type instances'''.  (It's worth noting, though, that there is already no support for coincident overlap between branched type instances, or between a singleton type instance and a branched one; it is currently only supported between singleton type instances.) 
     73 
     74Plan (B) above has a better relationship with coincident overlap, but not quite a rosy one: in the event that an infinite type is needed to show the overlap, we don't have a well-defined substitution to apply to the RHS. It is conceivable to allow coincident overlap only when the unification algorithm produces a bona fide substitution. But, there may be no need for this. 
    6075 
    6176However, we can recover coincident overlap with in a branched instance: see [wiki:NewAxioms/CoincidentOverlap here].  
    6277 
    63  
    64 == Problem: branched instances == 
    65  
    66 But, how does this interact with branched instances (those new instance forms that allow for ordered overlapping)? We still need nonlinear branched instances, as the canonical example of a nonlinear instance is an equality test: 
    67 {{{ 
    68 type family Equals a b :: Bool 
    69  
    70 type instance where 
    71   Equals x x = True 
    72   Equals x y = False 
    73 }}} 
    74 ... 
    75  
    76 The solution is to declare a ''type space'' that all branches fit within. 
    77  
    78 For example:  
    79 {{{ 
    80 type family Equals a b :: Bool 
    81  
    82 type instance Equals x y where 
    83   Equals x x = True 
    84   Equals x y = False 
    85 }}} 
    86 The header "`type instance Equals x y`" declares the "type space" of the declaration; the `where` part says how to match calls within that type space (top to bottom). 
    87  
    88 In this case the type space is the whole space, but that need not be the case: 
    89 {{{ 
    90 type family F a b :: * 
    91  
    92 type instance F Int x where 
    93   F Int Bool = Double 
    94   F Int Int  = Char 
    95   F Int a    = Bool 
    96  
    97 type instance F Bool y = Int 
    98 }}} 
    99 Here the first `type instance` covers calls of form `(F Int x)`, while the second covers 
    100 calls of form `(F Bool y)`. 
    101  
    102 All the equations in the `where` part must be part of (i.e. an instance of) the  
    103 type space declared in the header.  For example, this will be disallowed: 
    104  
    105 {{{ 
    106 type instance Bad [x] y where 
    107   Bad [Int] Int = Bool -- OK 
    108   Bad a     b   = ()   -- not OK: outside the type space (Bad [x] y) 
    109 }}} 
    110  
    111 The declared type space will be checked for overlap with other instances using the same linearization check that unbranched instances use. 
    112  
    11378== Concrete Proposal == 
    11479 
    115  * Among unbranched instances, check linearized forms of the LHS of instances when doing overlap checking. Thus, our two problematic instances of {{{F}}}, at the top, will conflict. 
     80 * Use plan (B) to check for overlap. Thus, our two problematic instances of {{{F}}}, at the top, will conflict. 
    11681 
    117  * After linearizing a left-hand side, the right-hand side of the instance is ill-defined. Thus, the current coincidence check (see [wiki:NewAxioms/CoincidentOverlap here] for more information) is no longer possible and will be removed. (Don't yell yet. Keep reading.) 
     82 * The current coincidence check (see [wiki:NewAxioms/CoincidentOverlap here] for more information) is no longer straightforward and will be removed. (Don't yell yet. Keep reading.) 
    11883 
    11984 * Allow coincident overlap within branched instances. This recovers the lost coincident overlap check on unbranched instances. See [wiki:NewAxioms/CoincidentOverlap here] for more information. 
    12085 
    121  * Optional: Add type space declarations to the {{{type instance where}}} syntax, checking to make sure that branches fit within the declared space. [wiki:NewAxioms/TypeSpaces This page] has the details. 
    122  
    123  * Optional: Add new syntax {{{type family Foo a b where { Foo ... = ... ; Foo ... = ... } }}} to declare a type family with one branched instance covering the entire type space. This would be a ''closed'' type family. 
    124  
    125 == Discussion about coincident overlap == 
    126  
    127 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. 
    128  
    129 To see why disallowing coincident overlap checking for unbranched axioms is vitally necessary, consider this example: 
    130  
    131 {{{ 
    132 type instance F a a Int = a 
    133 type instance F c d d   = Int 
    134 }}} 
    135  
    136 This overlap is most certainly are not OK (think about {{{F G G G}}}, where this is the malignant {{{G}}} from the beginning of this page), but they do coincide in the region of overlap. Yuck Yuck! So, we give up and just say "no" to coincident overlap in this case. 
     86 * Optional: Change the syntax for branched family instances, as described [wiki:NewAxioms/ClosedTypeFamilies here]. 
    13787 
    13888== Alternative (Non-)Solution ==