|Version 1 (modified by AntC, 3 years ago) (diff)|
Discussion: Pattern-matching axioms
At Pedro's invitation, comment/suggestions/requests for clarification/alternative solutions, to explore the design space.
- Organised into sub-headings: as and when these grow, split into sub-pages.
Requests for Clarification
According to [Bulatz as of 2007] http://www.haskell.org/haskellwiki/GADTs_for_dummies:
"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."
- Instance Priorities/Selection order is essentially this Pattern-matching axioms approach.
- 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.
This is using Constraint Handling Rules (implemented through Chameleon) to guide type inference. Example of instances using guards:
type instance Equal a a = True -- regular instance type instance Equal a b | a /~ b = False -- guarded instance, using type dis-equality
- Instances do not have to appear in any particular order; do not have to be defined together (nor even in the same module).
- The syntax mimics pattern guards for function bindings, using /~ per type equality constraints.
- But the guards are not constraints: they control whether the instance is selected (whereas constraints validate the types after the instance has been selected).
- Instances must not overlap (after taking the disequalities into account), so we can't crete unsound FC coercions.
Example Applications/Uses for Instance Overlap
- Strongly typed heterogeneous collections (colloquially known as HLists). Kiselyov, Lammel, Schupke 2004.
Section 6 Ended up in murky water with overlaps. Section 9 discusses approaches to make overlapping less fragile (and specifically TTypeable - Type-level Type representations.
- Data Types a la Carte. Swierstra 2008. An approach to Wadler's Expression Problem.
Section 4 discusses limitations caused by overlaps. http://wadler.blogspot.co.nz/2008/02/data-types-la-carte.html discusses those limitations, with some solutions suggested.
- Monad Transformers/Library. ??
(I believe) Monad Transformers originally used overlaps extensively, and were then re-engineered to avoid difficulties. What difficulties? How/why re-engineered? Would the earlier approach be workable under Pattern-matching? Would it be more user-friendly than the later approach?