Changes between Version 1 and Version 2 of NewAxioms/DiscussionPage


Ignore:
Timestamp:
May 30, 2012 12:21:36 PM (3 years ago)
Author:
AntC
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/DiscussionPage

    v1 v2  
    55 * Organised into sub-headings: as and when these grow, split into sub-pages. 
    66 
     7 * Please add further comment/detail. And correct anything I've mis-represented [AntC]. 
     8 
    79== Requests for Clarification == 
    810 
     11 * Is it possible to have more than one grouping for a given type function? (Possibly declared in separate modules.) Example: 
     12 
     13{{{ 
     14module M1 where 
     15    type instance H Int b  where 
     16        ... -- sequence of patterns to dis-overlap on b 
     17 
     18module M2 where 
     19    type instance H Char b where 
     20        ... -- sequence of unrelated patterns on b 
     21}}} 
     22 
     23  (Section 3.3 Transltion of the draft design/Law 3.5 (Consistent instances) seems to be saying multiple groupings are OK. An example would make it clearer.) 
     24 
     25 * Are there any rules/validation around the sequence of patterns within a grouping? 
     26 
     27  If a later pattern is more specific than an earlier (so could never get selected) is that pattern flagged, or just (in effect) silently ignored? 
     28 
    929== Suggestions == 
     30 
     31 * '''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. 
     32 
     33{{{ 
     34hCons :: (Lacks e l) => e -> l -> HCons e l          -- smart constructor, validate that l doesn't already contain e 
     35hCons = HCons                                        -- then we can do type-indexed lookup on the HList 
     36 
     37class Lacks e l                                      -- constraint only, no methods 
     38instance Lacks e HNil                                -- got to the end of the HList, not found an element type e 
     39instance (NoneSuch e) => Lacks e (HCons e l')        -- make this a fail by imposing an unfulfillable constraint 
     40instance (Lacks e l') => Lacks e (HCons e' l')       -- this element doesn't match, recurse on the tail 
     41 
     42-- possible instance grouping approach: 
     43 
     44hCons :: (Lacks e l ~ True) => e -> l -> HCons e l   -- what error reporting does this give when e found in l? 
     45 
     46type instance Lacks e l where 
     47    Lacks e HNil = True 
     48    Lacks e (HCons e l') = False 
     49    Lacks e (HCons e' l') = Lacks e l' 
     50 
     51-- disequality guards seem to show the intent more clearly: 
     52type instance Lacks e HNil = True 
     53type instance Lacks e (HCons e' l')  | e /~ e'   = Lacks e l'   -- no instance for the equality 
     54}}} 
     55 
    1056 
    1157== Alternative Solutions == 
     
    1561  "In many other cases [of overlap] this automatic [instance] selection is not powerful enough and we are forced to use some artificial tricks or complain to the language developers. The two most well-known language extensions proposed to solve such problems are instance priorities, which allow us to explicitly specify instance selection order, and '/=' constraints, which can be used to explicitly prohibit unwanted matches." 
    1662 
    17  * '''Instance Priorities/Selection order''' is essentially this Pattern-matching axioms approach. 
     63==== Instance Priorities/Selection order ==== 
    1864 
    19  * '''Disequality''' ''constraints'' (probably better called '''Guards''' or '''Restraints''' to avoid confusion with Class and type equality Constraints) date from at least '''A Theory of Overloading'''. Sulzmann & Stuckey 2002. Section 8.2 '''Overlapping Definitions'''. 
     65Is essentially this Pattern-matching axioms approach. 
     66 
     67  '''Instance Chains: Type Class Programming Without Overlapping Instances'''. Morris & Mark P.Jones 2010. contains some similar ideas, but in context of Functional Dependencies. (It also supports Class constraints being used to select patterns, and provides a ''fail'' outcome that triggers backtracking search for a better-matching instance.) 
     68 
     69==== Disequality ''constraints'' ==== 
     70 
     71(Probably better called '''Guards''' or '''Restraints''' to avoid confusion with Class and type equality Constraints) date from at least '''A Theory of Overloading'''. Sulzmann & Stuckey 2002. Section 8.2 '''Overlapping Definitions'''. 
    2072 
    2173  This is using Constraint Handling Rules (implemented through Chameleon) to guide type inference. Example of instances using guards: 
     
    2880  '''Note:''' 
    2981 
    30  * Instances do not have to appear in any particular order; do not have to be defined together (nor even in the same module). 
     82   * Instances do not have to appear in any particular order; do not have to be defined together (nor even in the same module). 
    3183 
    32  * The syntax mimics pattern guards for function bindings, using /~ per type equality constraints. 
     84   * The syntax mimics pattern guards for function bindings, using /~ per type equality constraints. 
    3385 
    34  * But the guards are not constraints: they control whether the instance is selected (whereas constraints validate the types after the instance has been selected). 
     86   * But the guards are not constraints: they control whether the instance is selected (whereas constraints validate the types after the instance has been selected). 
    3587 
    36  * Instances must not overlap (after taking the disequalities into account), so we can't crete unsound FC coercions. 
     88   * Instances must not overlap (after taking the disequalities into account), so we can't create unsound FC coercions. 
     89 
     90==== Type-level Type Representations (TTypeable) ==== 
     91 
     92Oleg Kiselyov 2004 (part of the HList work, Section 9 of the paper) 
     93 
     94  Translates every type in your code to a cannonical type representation (based on type-level naturals), then you can compare the representaions for equality (and indeed induce an ordering). 
     95 
     96   * One downside is that you have to provide a translation instance for each user-defined type, and make sure the representation doesn't clash with any other type. Template Haskell helps, compiler support would be better. 
    3797 
    3898== Comments == 
     99 
     100 * '''Instance validation''' for type families is 'eager' -- that is, each instance is validated for overlap at point of declaration. 
     101   * 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.) 
     102   * GHC behaves like that because your code might not have an irresolvable use, so it's trying to be generous. 
     103   * Or GHC might select different instances for what seem like the same uses. 
     104   * Compiler flag IncoherentInstances is a good way to make this effect worse. 
     105   * BTW Hugs' validation for overlaps is eager. 
     106 
     107 * '''Sudden and Silent Overlap:''' a newly-imported module or package might declare an instance (for a type class, especially a library class) that is more specific than any you've been working with. The program's behaviour may suddenly change for no (apparent) reason. 
     108 
     109  (??The original Monad Transformers approach suffered from this. The design deliberately had a most general instance declared with the class. Application modules overrode it.) 
     110 
    39111 
    40112== Example Applications/Uses for Instance Overlap == 
     
    53125 
    54126== References and Links == 
     127 
     128[To do ...] 
     129 
     130Surprisingly few wiki pages discuss overlaps. 
     131 
     132Link to GHC flags on OverlappingInstances, IncoherentInstances, (and possibly UndecidableInstances). 
     133 
     134See Haskell-cafe and Haskell-prime mailing lists anon.