Changes between Version 11 and Version 12 of NewAxioms


Ignore:
Timestamp:
Jun 8, 2012 8:12:50 AM (3 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms

    v11 v12  
    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.  Here's the idea:
     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, but do look at the Latex document pointed to from the top of this page for details.
    5151
    5252 *  A `type instance` declaration can define multiple equations, not just one:
     
    8383}}}
    8484  Here the second equation can never match.
     85
     86 * The equations do not need to share a common pattern:
     87{{{
     88type instance F where
     89  F Int = Char
     90  F (a,b) = Ing
     91}}}
     92
    8593 
     94== Questions of syntax ==
     95
     96What should the "header" look like? 
     97{{{
     98(A)      type instance where      -- Use "where"
     99            F (a,b)   = [Char]
     100            F (Int,b) = Char
     101            f Bool    = Char
     102
     103(B)      type instance of         -- Use "of" (yuk)
     104            F (a,b)   = [Char]
     105            F (Int,b) = Char
     106            f Bool    = Char
     107
     108(C)      type instance F where     -- Redundantly mention F in the header
     109            F (a,b)   = [Char]
     110            F (Int,b) = Char
     111            f Bool    = Char
     112}}}
     113We need one of the existing "layout herald" keywords (`of`, `let`, `where`) to smoothly support the nested block of equations.  It's not clear whether or not it is useful to mention the name of the function in the header.