Changes between Version 9 and Version 10 of NewAxioms


Ignore:
Timestamp:
Jun 7, 2012 12:55:09 PM (3 years 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