Version 2 (modified by pigworker, 5 years ago) (diff) |
---|

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.

Much of the motivation for this proposal can be found in 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. Max Bolingbroke, commenting on context aliases? 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.

Concretely, the proposal is to

- add a kind
`Fact`for constraints, so that, e.g.`Monad :: (* -> *) -> Fact`; - close
`Fact`under tuples, so`(F1, .. Fn) :: Fact`iff each`Fi :: Fact`; - allow nested tuple constraints, with componentwise unpacking and inference, so if
`Stringy x = (Read x, Show x)`, then`(Stringy x, Eq x)`is a valid constraint without flattening it to`(Read x, Show x, Eq x)`; - allow (rather, neglect to forbid) the use of
`type`to introduce synonyms for Fact(-constructing) things; - retain the policy of defaulting to kind
`*`in ambiguous inference problems -- notably`()`is the unit type and the trivial constraint -- except where overridden by kind signatures.

Examples:

type Stringy x = (Read x, Show x) type Transposable f = (Traversable f, Applicative f) type Reduce m x = (Monad m, Monoid (m x)) type MyUnit = () -- gives the unit type by default type MyTrue = () :: Fact -- needs the kind signature to override the default

One might consider a syntax for giving fully explicit kinds to type synonyms, like this:

type Reduce :: (* -> *) -> * -> Fact where Reduce m x = (Monad m, Monoid (m x))

We should also find that the **type family** mechanism extends to the new kinds, pretty much straight out of the box. For example:

type family HasDerivatives n f :: Fact type instance HasDerivatives Z f = () type instance HasDerivatives (S n) f = (Differentiable f, HasDerivatives n (D f))

where `Differentiable` is the class of differentiable functors and `D f` is the associated derivative functor.

Bikeshed: `Fact` is the working name for the new kind. `Constraint` is an obvious contender, but long. `Prop` should *not* be used, as any analogy to Prop in the Calculus of Constructions would be bogus: proofs of a Prop are computationally irrelevant and discarded by program extraction, but witnesses to a Fact are material and computationally crucial. Another thought: 'Constraint' sounds more like a requirement than a guarantee, whereas 'Fact' is neutral. On the other hand, the kinding `F :: Fact` might be misleadingly suggestive of `F`'s truth, over and above its well-formedness.