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

KindFact
v6 v7 13 13 * Allow (rather, neglect to forbid) the use of {{{type}}} to introduce synonyms for Fact(constructing) things. Thus one might say 14 14 {{{ 15 type Transposable f = (Traversable f, Applicative f) 16 type Reduce m x = (Monad m, Monoid (m x)) 15 17 type Stringy x = (Read x, Show x) 18 }}} 19 20 * Allow these synonym facts to appear wherever a class constraint can appear. For example 21 {{{ 22 class Stringy a => C a where .... 23 f :: Reduce m x => x > m x 16 24 }}} 17 25 18 26 * 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)}}}. 19 27 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: 24 29 {{{ 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))28 30 type MyUnit = ()  gives the unit type by default 29 31 type MyTrue = () :: Fact  needs the kind signature to override the default 30 32 }}} 33 34 * Allow the '''type family''' mechanism to extend to the new kinds, pretty much straight out of the box. For example: 35 {{{ 36 type family HasDerivatives n f :: Fact 37 type instance HasDerivatives Z f = () 38 type 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 == 31 43 32 44 One might consider a syntax for giving fully explicit kinds to type synonyms, like this: … … 36 48 }}} 37 49 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 45 51 46 52 == Bikeshed discussion of nomenclature == 47 53 48 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 wellformedness.