3 | | Proposal: extend the kind system with a kind '''Fact''' to cover constraints as well as types, in order to reuse existing abstraction mechanisms, notably '''type synonyms''', in the constraint language. |
| 3 | This page describes an extension to kind system that supporsts a |
| 4 | kind '''Constraint''' to cover constraints as well as types, in |
| 5 | order to reuse existing abstraction mechanisms, notably '''type |
| 6 | synonyms''', in the constraint language. |
5 | | Much of the motivation for this proposal can be found in [http://www.cs.kuleuven.be/%7Etoms/Research/papers/constraint_families.pdf Haskell Type Constraints Unleashed] which identifies the shortage of abstraction mechanisms for constraints relative to types. See ticket #788 for the resulting '''constraint synonym''' proposal, which seeks to fill some of the gaps with new declaration forms. Here, however, the plan is to extend the kind system, empowering the existing mechanisms to work with constraints. [http://blog.omega-prime.co.uk/?p=61 Max Bolingbroke], commenting on [http://www.haskell.org/haskellwiki/Context_alias context aliases] (in turn based on John Meacham's [http://repetae.net/recent/out/classalias.html class alias] proposal) makes a similar suggestion, remarking that a new kind would probably help. The claim here is that the new kind obviates the need for other new syntax. |
| 8 | Much of the motivation for this proposal can be found in [http://www.cs.kuleuven.be/%7Etoms/Research/papers/constraint_families.pdf Haskell Type Constraints Unleashed] which identifies the shortage of abstraction mechanisms for constraints relative to types. See ticket #788 for the resulting '''constraint synonym''' proposal, which seeks to fill some of the gaps with new declaration forms. Here, however, the plan is to extend the kind system, empowering the existing mechanisms to work with constraints. [http://blog.omega-prime.co.uk/?p=61 Max Bolingbroke], commenting on [http://www.haskell.org/haskellwiki/Context_alias context aliases] (in turn based on John Meacham's [http://repetae.net/recent/out/classalias.html class alias] proposal) makes a similar suggestion, remarking that a new kind would probably help. The final design is largely the work of Conor McBride. |
84 | | [illissius] I checked thesaurus.com for (even remotely) plausible names, and this is what I found: |
85 | | * Fact, Knowledge, Information, Data, Evidence, Proof |
86 | | * Requirement, Constraint, Guarantee, Promise, Contract |
87 | | * Characteristic, Attribute, Property, Trait, Capability |
88 | | * Axiom, Lemma, Theorem, Proposition, Postulate, Premise, Claim, Posit |
| 105 | A major change is that the data type `Type` (in module `TypeRep`) no longer has |
| 106 | a `PredTy` construct. Instead, we have just `Type`: |
90 | | [JonasDuregard] What about Context? That is after all the "official" name for the collections of constraints that appear in type signatures. |
91 | | [illissius] I like it. |
| 108 | * In a function type `t1 -> t2`, the arguent `t1` is a ''constraint argument'' iff `t1 :: Constraint`. |
| 109 | |
| 110 | * Constraint arguments are pretty-printed before a double arrow "`=>`" when displaying types. Moreover they are passed implicitly in source code; for exmaple if `f :: ty1 => ty2 -> ty3` then the Haskell programmer writes a call `(f e2)`, where `e2 :: ty2`, and the compiler fills in the first argument of type `ty1`. |
| 111 | |
| 112 | * A constraint type (of kind `Constraint`) can take one of these forms |
| 113 | * '''Equality constraint''': `TyConApp eqTyCon [ty1, ty2]` |
| 114 | * '''Class constraint''': `TyConApp tc [ty1, ty2]`, where `tc` is a `TyCon` whose `classTyCon_maybe` is `Just cls`. |
| 115 | * '''Implicit parameter''': `TyConApp tc [ty1]`, where `tc` is a `TyCon` whose `tyConIP_maybe` is `Just ip`. |
| 116 | * '''Constraint variable''': `TyVarTy tv` where `tv` has kind `Constraint`. |
| 117 | * '''Tuple constraint''': `TyConApp tup_tc [ty1, ..., tyn]`, where `tup_tc` is a constraint tuple `TyCon`. |
| 118 | |
| 119 | * Implicit parameters have a type written `?x::Int`, say. Concretely, this is represented as `TyConApp ?x [intTy]`, where `intTy` is the representation of the type for `Int`, and `?x` is a `TyCon` of kind `(* -> *)`. There is an infinite family of such implicit-parameter `TyCon`s; see data constructor `IPTyCon` in data type `TyConParent` in `TyCon`. |
| 120 | |
| 121 | * Constraint types (ie types with kind `Constraint`) are always boxed, including equality constraints. So `(a ~ b)` is a ''boxed'' value. We also have a primtive type of ''unboxed'' equality constraints, written `(a ~# b)`. Roughly the former is declared thus: |
| 122 | {{{ |
| 123 | data a ~ b = Eq# (a ~# b) |
| 124 | }}} |
| 125 | where `Eq#` is a data constructor with a single, unboxed, zero-width field of type `(a ~# b)`. See `TysWiredIn.eqTyCon`. |
| 126 | |
| 127 | * The constraint solver in the type checker deals solely in terms of boxed constraints. |
| 128 | |
| 129 | * Constraint tup |