Changes between Version 5 and Version 6 of KindFact


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

--

Legend:

Unmodified
Added
Removed
Modified
  • KindFact

    v5 v6  
    1111  * Close {{{Fact}}} under tuples, so {{{(F1, .. Fn) :: Fact}}} iff each {{{Fi :: Fact}}}.
    1212
    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{{{
     15type Stringy x = (Read x, Show x)
     16}}}
    1417
    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)}}}.
    1619
    1720  * 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.
     
    4144where {{{Differentiable}}} is the class of differentiable functors and {{{D f}}} is the associated derivative functor.
    4245
    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 well-formedness.
     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 well-formedness.