Version 8 (modified by 6 years ago) (diff) | ,
---|

# Adding Kind Fact

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 (in turn based on John Meacham's 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.

## The proposal

- 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 (rather, neglect to forbid) the use of
`type`

to introduce synonyms for Fact(-constructing) things. Thus one might saytype Transposable f = (Traversable f, Applicative f) type Reduce m x = (Monad m, Monoid (m x)) type Stringy x = (Read x, Show x)

- Allow these synonym facts to appear wherever a class constraint can appear. For example
class Stringy a => C a where .... f :: Reduce m x => x -> m x

- Allow nested tuple constraints, with componentwise unpacking and inference, so that
`(Stringy x, Eq x)`

is a valid constraint without flattening it to`(Read x, Show x, Eq x)`

.

- 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. For example:type MyUnit = () -- gives the unit type by default type MyTrue = () :: Fact -- needs the kind signature to override the default

- Allow the
**type family**mechanism to extend 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.

## More syntax

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))

## Discussion

`Fact`

synonyms appear to overlap with superclases. For example one could say

class (Read x, Show x) => Stringy x where {}

But there are significant differences

- Using the class mechanism forces you to give an
`instance`

declaration too. Perhaps something likeinstance (Read x, Show x) => Stringy x where {}

This is painful duplication, and (worse) there is little to stop you writing an overlapping instance later. At least, looking at the instance doesn't tell you that no overlapping instance is intended.

- The type family mechamism gives new power. For example, consider the celebrated collection example:
class Collection c where type family X c :: * -> Fact empty :: c a insert :: (X c) => c a -> a -> c a instance Collection [] where type instance X [] a = Eq a insert xs x = ... instance Collection Data.Set where type instance X Data.Set a = Ord a insert s x = ...

See Bulk types with class.

## Bikeshed discussion of nomenclature

`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.