# Changes between Version 6 and Version 7 of KindFact

Show
Ignore:
Timestamp:
03/09/11 17:15:00 (2 years ago)
Comment:

--

Unmodified
Removed
Modified
• ## KindFact

v6 v7
1313  * Allow (rather, neglect to forbid) the use of {{{type}}} to introduce synonyms for Fact(-constructing) things.  Thus one might say
1414{{{
15type Transposable f = (Traversable f, Applicative f)
16type Reduce m x = (Monad m, Monoid (m x))
1517type Stringy x = (Read x, Show x)
18}}}
19
20  * Allow these synonym facts to appear wherever a class constraint can appear.  For example
21{{{
22class Stringy a => C a where ....
23f :: Reduce m x => x -> m x
1624}}}
1725
1826  * 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)}}}.
1927
20   * 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.
21
22 Examples:
23
28  * 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:
2429{{{
25 type Stringy x = (Read x, Show x)
26 type Transposable f = (Traversable f, Applicative f)
27 type Reduce m x = (Monad m, Monoid (m x))
2830type MyUnit = () -- gives the unit type by default
2931type MyTrue = () :: Fact  -- needs the kind signature to override the default
3032}}}
33
34  * Allow the '''type family''' mechanism to extend to the new kinds, pretty much straight out of the box. For example:
35{{{
36type family   HasDerivatives n     f :: Fact
37type instance HasDerivatives Z     f  = ()
38type instance HasDerivatives (S n) f  = (Differentiable f, HasDerivatives n (D f))
39}}}
40  where {{{Differentiable}}} is the class of differentiable functors and {{{D f}}} is the associated derivative functor.
41
42== More syntax ==
3143
3244One might consider a syntax for giving fully explicit kinds to type synonyms, like this:

3648}}}
3749
38 We should also find that the '''type family''' mechanism extends to the new kinds, pretty much straight out of the box. For example:
39 {{{
40 type family   HasDerivatives n     f :: Fact
41 type instance HasDerivatives Z     f  = ()
42 type instance HasDerivatives (S n) f  = (Differentiable f, HasDerivatives n (D f))
43 }}}
44 where {{{Differentiable}}} is the class of differentiable functors and {{{D f}}} is the associated derivative functor.
50
4551
4652== Bikeshed discussion of nomenclature ==
4753
48  {{{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.
54{{{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.