# Changes between Version 5 and Version 6 of KindFact

Ignore:
Timestamp:
Mar 10, 2011 1:00:35 AM (7 years ago)
Comment:

--

Unmodified
Removed
Modified
• ## KindFact

 v5 * 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.  Thus one might say {{{ type Stringy x = (Read x, Show x) }}} * Allow (rather, neglect to forbid) the use of {{{type}}} to introduce synonyms for Fact(-constructing) things. * 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. 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. == 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.