Changes between Version 5 and Version 6 of NewAxioms/DiscussionPage


Ignore:
Timestamp:
Jun 11, 2012 5:07:50 AM (3 years ago)
Author:
AntC
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/DiscussionPage

    v5 v6  
    1010== Suggestions == 
    1111 
    12  * '''Instance match fail:''' There are use cases where we want to make the existence of a more specific match a type-level failure. Currently this needs 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 type-level 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. 
    1313 
    1414{{{ 
     
    3636 
    3737 
    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: 
    3939{{{ 
    4040    type family Equal a b :: Bool where 
     
    119119{{{ 
    120120    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) 
    124124}}} 
    125125 
     
    130130  Presumably common-or-garden type instances can be generalised to instance groups, and different instance groups can be unified providing their patterns don't overlap. Like this: 
    131131 
     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}}} 
    132156 
    133157== Example Applications/Uses for Instance Overlap ==