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.