Changes between Version 3 and Version 4 of KindFact


Ignore:
Timestamp:
Mar 10, 2011 12:57:56 AM (3 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • KindFact

    v3 v4  
     1= Adding Kind Fact = 
     2 
    13Proposal: extend the kind system with a kind '''Fact''' to cover constraints as well as types, in order to reuse existing abstraction mechanisms, notably '''type synonyms''', in the constraint language. 
    24 
    35Much of the motivation for this proposal can be found in [http://www.cs.kuleuven.be/%7Etoms/Research/papers/constraint_families.pdf Haskell Type Constraints Unleashed] which identifies the shortage of abstraction mechanisms for constraints relative to types. See ticket #788 for the resulting '''constraint synonym''' proposal, which seeks to fill some of the gaps with new declaration forms. Here, however, the plan is to extend the kind system, empowering the existing mechanisms to work with constraints. [http://blog.omega-prime.co.uk/?p=61 Max Bolingbroke], commenting on [http://www.haskell.org/haskellwiki/Context_alias context aliases] (in turn based on John Meacham's [http://repetae.net/recent/out/classalias.html class alias] proposal) makes a similar suggestion, remarking that a new kind would probably help. The claim here is that the new kind obviates the need for other new syntax. 
    46 
    5 Concretely, the proposal is to 
     7== The proposal ==  
    68 
    7   * add a kind {{{Fact}}} for constraints, so that, e.g. {{{Monad :: (* -> *) -> Fact}}}; 
    8   * close {{{Fact}}} under tuples, so {{{(F1, .. Fn) :: Fact}}} iff each {{{Fi :: Fact}}}; 
    9   * 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)}}}; 
    10   * allow (rather, neglect to forbid) the use of {{{type}}} to introduce synonyms for Fact(-constructing) things; 
    11   * 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. 
     9  * Add a kind {{{Fact}}} for constraints, so that, e.g. {{{Monad :: (* -> *) -> Fact}}}; 
     10  * Close {{{Fact}}} under tuples, so {{{(F1, .. Fn) :: Fact}}} iff each {{{Fi :: Fact}}}; 
     11  * 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)}}}; 
     12  * Allow (rather, neglect to forbid) the use of {{{type}}} to introduce synonyms for Fact(-constructing) things; 
     13  * 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. 
    1214 
    1315Examples: