Changes between Version 5 and Version 6 of NewAxioms/DiscussionPage
 Timestamp:
 Jun 11, 2012 5:07:50 AM (4 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

NewAxioms/DiscussionPage
v5 v6 10 10 == Suggestions == 11 11 12 * '''Instance match fail:''' There are use cases where we want to make the existence of a more specific match a typelevel failure. Currently thisneeds fudging with fake instances and constraints, leading to mystifying messages. The example is HList Lacks constraint.12 * '''Instance match fail:''' There are use cases where we want to make the existence of a more specific match a typelevel failure. (Compare this http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions/TotalFamilies#Definingtotalfamilies from Chak 2008, using VOID for the same purpose.) Currently a 'dead end' needs fudging with fake instances and constraints, leading to mystifying messages. The example is HList Lacks constraint. 13 13 14 14 {{{ … … 36 36 37 37 38 * '''Idiom of total instance''' (this would apply to all the HList examples). We only need one instance group for the whole; then it's the type family decl that seems superfluous. Perhaps we could allow:38 * '''Idiom of a total function''' (this would apply to all the HList examples). We only need one instance group for the whole family; then putting both decls seems superfluous. Perhaps we could conflate them: 39 39 {{{ 40 40 type family Equal a b :: Bool where … … 119 119 {{{ 120 120 type instance F Int Bool = ...  (1) is totally overlapped by (2), (3) and (4) 121 type instance F Int b = ... (2) partially overlaps (3)122 type instance F a Bool = ... (3)123 type instance F a b = ... (4) totally overlaps (1), (2) and (3)121 type instance F Int b = ...  (2) partially overlaps (3) 122 type instance F a Bool = ...  (3) 123 type instance F a b = ...  (4) totally overlaps (1), (2) and (3) 124 124 }}} 125 125 … … 130 130 Presumably commonorgarden type instances can be generalised to instance groups, and different instance groups can be unified providing their patterns don't overlap. Like this: 131 131 132 {{{ 133 type instance G (c, d) Int = c  generalise to type instance G where ... 134 type instance G Bool b = b  generalise likewise 135 136  now unify: 137 type instance G where 138 G (c, d) b = c 139 G Bool b = b  no overlap 140 141  take an instance with disequality guards: 142 type instance G a b  a /~ (_, _), a /~ Bool = a 143  generalise: 144 type instance G where 145 G (_, _) b = VOID 146 G Bool b = VOID 147 G a b = a 148 149  unify with the group above (observing overlaps): 150 type instance G where 151 G (c, d) b = c 152 G Bool b = b 153 G a b = a 154 155 }}} 132 156 133 157 == Example Applications/Uses for Instance Overlap ==