Changes between Version 9 and Version 10 of NewAxioms


Ignore:
Timestamp:
Jun 7, 2012 12:55:09 PM (23 months ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms

    v9 v10  
    4848== What to do about it == 
    4949 
    50 So the deficiency is in System FC, and it seems fundamental.  We've been working on an extension to System FC, with a corresponding source-language extension, that does allow overlapping type families, with care. You would write something like this: 
     50So the deficiency is in System FC, and it seems fundamental.  We've been working on an extension to System FC, with a corresponding source-language extension, that does allow overlapping type families, with care.  Here's the idea: 
     51 
     52 *  A `type instance` declaration can define multiple equations, not just one: 
    5153{{{ 
    52 type instance where 
     54type instance Eq where 
    5355  Equal a a = True 
    5456  Equal a b = False 
    5557}}} 
    5658 
     59 * Patterns within a single `type instance` declaration (henceforth "group") may overlap, and are matched top to bottom. 
     60 
     61 * A single type family may, as now, have multiple `type instance` declarations: 
     62{{{ 
     63type family F a :: * 
     64 
     65type instance F where 
     66  F [Int] = Int 
     67  F [a]   = Bool 
     68 
     69type instance F where 
     70  F (Int,b) = Char 
     71  F (a,b)   = [Char] 
     72}}} 
     73 
     74 * The groups for `F` may not overlap.  That is, there must be no type `t` such that `(F t)` matches both groups. 
     75 
     76 * The groups do not need to be exhaustive.   If there is no equation that matches, the call is stuck. (This is exactly as at present.) 
     77 
     78 * It would perhaps be possible to emit warnings for equations that are shadowed: 
     79{{{ 
     80type instance F where 
     81  F (a,b)   = [Char] 
     82  F (Int,b) = Char 
     83}}} 
     84  Here the second equation can never match. 
     85   
    5786 
    5887 
    5988 
     89