Changes between Version 6 and Version 7 of KindFact


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

--

Legend:

Unmodified
Added
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.