Changes between Version 11 and Version 12 of NewAxioms
 Timestamp:
 Jun 8, 2012 8:12:50 AM (3 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

NewAxioms
v11 v12 48 48 == What to do about it == 49 49 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 sourcelanguage extension, that does allow overlapping type families, with care. Here's the idea :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 sourcelanguage 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. 51 51 52 52 * A `type instance` declaration can define multiple equations, not just one: … … 83 83 }}} 84 84 Here the second equation can never match. 85 86 * The equations do not need to share a common pattern: 87 {{{ 88 type instance F where 89 F Int = Char 90 F (a,b) = Ing 91 }}} 92 85 93 94 == Questions of syntax == 95 96 What 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 }}} 113 We 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.