Changes between Version 11 and Version 12 of NewAxioms


Ignore:
Timestamp:
Jun 8, 2012 8:12:50 AM (23 months 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.