Changes between Version 7 and Version 8 of NewAxioms/DiscussionPage


Ignore:
Timestamp:
Jun 11, 2012 6:06:50 AM (22 months ago)
Author:
AntC
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/DiscussionPage

    v7 v8  
    2525hCons :: (Lacks e l ~ True) => e -> l -> HCons e l   -- what error reporting does this give when e found in l? 
    2626 
    27 type instance Lacks e l where 
     27type family Lacks e l :: Bool 
     28type instance Lacks where 
    2829    Lacks e HNil = True 
    2930    Lacks e (HCons e l') = False 
     
    4344 
    4445    type family HasMember a (b :: '[]) :: Bool where 
    45         HasMember a '[] = False                      -- (not overlapping) 
     46        HasMember a '[] = False                                  -- (not overlapping) 
    4647        HasMember a ( a ': bs ) = True 
    4748        HasMember a ( b ': bs ) = HasMember a bs 
     
    9394== Comparisons to other approaches with overlaps == 
    9495 
    95  * http://hackage.haskell.org/trac/ghc/wiki/TFvsFD [Thank you Etienne, and there's a very helpful '''See also'''.] Several examples where Type Functions don't seem to be as helpful as Type Classes/Constraints/FunDeps. Some of these examples need overlaps, but not all. Equality constraints seem to make type refinement more 'eager' than under TF's.  
    96  
    97  * http://okmij.org/ftp/Haskell/PeanoArithm.lhs [referenced from the TF vs FD discussion] 
     96 * http://hackage.haskell.org/trac/ghc/wiki/TFvsFD [Thank you Etienne, and there's a very helpful '''See also'''.] Several examples where Type Functions don't seem to be as powerful as Type Classes/Constraints/FunDeps. Some of these examples need overlaps, but not all. Equality constraints seem to make type refinement more 'eager' than under TF's.  
     97 
     98 * http://okmij.org/ftp/Haskell/PeanoArithm.lhs [referenced from the TF vs FD discussion] Exploits a bi-directional FunDep technique, to get subtraction of type-level Nats using only a definition of add. 
    9899 
    99100 
     
    101102 
    102103 * '''Instance validation''' for type families is 'eager' -- that is, each instance is validated for overlap at point of declaration. 
    103    * Contrast that instance validation (in GHC) for classes is 'negligent' (or 'generous' depending on your point of view: can't use the word 'lazy'): you can declare overlaps that compile OK, but then GHC complains at the use site that it has irresolvable overlaps. (The use site might be GHCi.) 
    104    * GHC behaves like that because your code might not have an irresolvable use, so it's trying to be generous. 
     104   * Contrast that instance validation (in GHC) for classes is 'negligent' (or 'relaxed', or 'generous' depending on your point of view: can't use the word 'lazy'): you can declare overlaps that compile OK, but then GHC complains at the use site that it has irresolvable overlaps. (The use site might be GHCi.) 
     105   * GHC behaves like that because your code's usages might all be resolvable, so it's trying to be generous. 
    105106   * Or GHC might select different instances for what seem like the same uses. 
    106107   * Compiler flag IncoherentInstances is a good way to make this effect worse. 
     
    126127  (For reasons I don't understand) when GHC introduced Associated Types (Families), they seemed particularly concerned about partial overlaps (and confluence thereof http://www.haskell.org/haskellwiki/GHC/Indexed_types section 6.2.2 Overlap). Compare that Hugs handles partial overlaps badly, so it's usually better to 'factor' into total overlaps. (That is: if you have instances like (2) and (3), add an instance like (1).) 
    127128 
    128   If you allow only total overlaps, validation of the instances seems more tractable, and the rules for selecting the instance at the use site would be more coherent (perhaps?). Is it the possibility of partial overlap that led to GHC's validation being more 'generous'/less eager? 
     129  If you allow only total overlaps, validation of the instances seems easier to understand, and the rules for selecting the instance at the use site would be more coherent (perhaps?). Is it the possibility of partial overlap that led to GHC's validation being more 'generous'/less eager? 
    129130 
    130131 * '''Generalisation and Unification of instance groups''' and disequality guards 
     
    133134 
    134135{{{ 
    135     type instance G (c, d) Int = c               -- generalise to        type instance G where ... 
    136     type instance G Bool b     = b               -- generalise likewise 
     136    type instance G (c, d) b   = c               -- generalise to 
     137    type instance G where ... 
     138    type instance G Bool   b   = b               -- generalise likewise 
    137139 
    138140    -- now unify: 
     
    173175== References and Links == 
    174176 
     177  See references scattered through the above discussions. 
     178 
    175179 * http://hackage.haskell.org/trac/ghc/wiki/TFvsFD#SeeAlso2 
    176180 
     
    178182 
    179183Surprisingly few wiki pages discuss overlaps. 
     184 * http://www.haskell.org/haskellwiki/GHC/AdvancedOverlap 
     185 * http://www.haskell.org/haskellwiki/Research_papers/Type_systems 
    180186 
    181187Link to GHC flags on OverlappingInstances, IncoherentInstances, (and possibly UndecidableInstances). 
     
    225231SCW: For these last two, it would be consistent with current treatment (and with multiple groups) to allow 'stuck' type families. Perhaps GHC could flag a few more bugs if the user could specify when a type family was expected to be fully covered, but I don't think that failing to do this check will jeopardize type soundness.   
    226232 
    227  * Arethe examples for the multi- type instance declarations quite as intended? The heads have no head, as it were. Is this allowed? 
     233 * Are the examples for the multi-type instance declarations quite as intended? The heads have no head, as it were. [That is as SPJ intended] Is this allowed? 
    228234{{{ 
    229235    type instance F [a] where ...