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 ==