Changes between Version 5 and Version 6 of KindFact
 Timestamp:
 Mar 10, 2011 1:00:35 AM (5 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

KindFact
v5 v6 11 11 * Close {{{Fact}}} under tuples, so {{{(F1, .. Fn) :: Fact}}} iff each {{{Fi :: Fact}}}. 12 12 13 * 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)}}}. 13 * Allow (rather, neglect to forbid) the use of {{{type}}} to introduce synonyms for Fact(constructing) things. Thus one might say 14 {{{ 15 type Stringy x = (Read x, Show x) 16 }}} 14 17 15 * Allow (rather, neglect to forbid) the use of {{{type}}} to introduce synonyms for Fact(constructing) things.18 * 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)}}}. 16 19 17 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. … … 41 44 where {{{Differentiable}}} is the class of differentiable functors and {{{D f}}} is the associated derivative functor. 42 45 43 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 wellformedness. 46 == Bikeshed discussion of nomenclature == 47 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 wellformedness.