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.