Changes between Version 11 and Version 12 of KindFact


Ignore:
Timestamp:
Sep 12, 2011 12:59:43 PM (3 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • KindFact

    v11 v12  
    1 = Adding Kind Fact = 
     1= Adding Kind `Constraint` = 
    22 
    3 Proposal: 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. 
     3This page describes an extension to kind system that supporsts a 
     4kind '''Constraint''' to cover constraints as well as types, in 
     5order to reuse existing abstraction mechanisms, notably '''type 
     6synonyms''', in the constraint language. 
    47 
    5 Much 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. 
     8Much 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 final design is largely the work of Conor McBride. 
    69 
    7 == The proposal ==  
     10The new design has now been implemented by Max Bolingbroke.  It's in HEAD and upcoming GHC 7.4, and is described in [http://blog.omega-prime.co.uk/?p=127 Max's Sept 2011 blog post]. 
    811 
    9   * Add a kind {{{Fact}}} for constraints, so that, e.g. {{{Monad :: (* -> *) -> Fact}}}. 
     12== The design: user's eye view ==  
    1013 
    11   * Close {{{Fact}}} under tuples, so {{{(F1, .. Fn) :: Fact}}} iff each {{{Fi :: Fact}}}. 
     14  * Add a kind {{{Constraint}}} for constraints, so that, e.g. {{{Monad :: (* -> *) -> Constraint}}}. 
    1215 
    13   * Allow (rather, neglect to forbid) the use of {{{type}}} to introduce synonyms for Fact(-constructing) things.  Thus one might say 
     16  * Close {{{Constraint}}} under tuples, so {{{(F1, .. Fn) :: Constraint}}} iff each {{{Fi :: Constraint}}}. 
     17 
     18  * Allow (rather, neglect to forbid) the use of {{{type}}} to introduce synonyms for Constraint(-constructing) things.  Thus one might say 
    1419{{{  
    1520type Transposable f = (Traversable f, Applicative f) 
     
    2934{{{ 
    3035type MyUnit = () -- gives the unit type by default 
    31 type MyTrue = () :: Fact  -- needs the kind signature to override the default 
     36type MyTrue = () :: Constraint  -- needs the kind signature to override the default 
    3237}}} 
    3338 
    3439  * Allow the '''type family''' mechanism to extend to the new kinds, pretty much straight out of the box. For example: 
    3540{{{ 
    36 type family   HasDerivatives n     f :: Fact 
     41type family   HasDerivatives n     f :: Constraint 
    3742type instance HasDerivatives Z     f  = () 
    3843type instance HasDerivatives (S n) f  = (Differentiable f, HasDerivatives n (D f)) 
     
    4045  where {{{Differentiable}}} is the class of differentiable functors and {{{D f}}} is the associated derivative functor. 
    4146 
    42 == More syntax == 
     47  * You can abtract over type variables of kind `Constraint`. Here is a contrived example: 
     48{{{ 
     49data T a where     -- Notice a :: Constraint 
     50  MkT :: a => T a  -- Note the cool type:  a => blah 
     51 
     52f :: T (Ord x) -> x -> Bool 
     53f MkT x = x > x 
     54 
     55g :: T (Ord Int) 
     56g = MkT 
     57 
     58main = print (f g 4)   -- Computes 4>4 = False 
     59}}} 
     60  We could do with some convincing examples of why this is a good thing, but it simply falls out. 
     61 
     62=== More syntax === 
    4363 
    4464One might consider a syntax for giving fully explicit kinds to type synonyms, like this: 
    4565{{{ 
    46 type Reduce :: (* -> *) -> * -> Fact where 
     66type Reduce :: (* -> *) -> * -> Constraint where 
    4767  Reduce m x = (Monad m, Monoid (m x)) 
    4868}}} 
    4969 
    50 == Discussion == 
     70=== Discussion === 
    5171 
    52 `Fact` synonyms appear to overlap with superclases.  For example one could say 
     72`Constraint` synonyms appear to overlap with superclases.  For example one could say 
    5373{{{ 
    5474class (Read x, Show x) => Stringy x where {} 
     
    6484{{{ 
    6585class Collection c where 
    66   type family X c :: * -> Fact 
     86  type family X c :: * -> Constraint 
    6787  empty :: c a 
    6888  insert :: (X c) => c a -> a -> c a 
     
    7898  See [http://research.microsoft.com/en-us/um/people/simonpj/papers/collections.ps.gz Bulk types with class]. 
    7999 
    80 == Bikeshed discussion of nomenclature == 
     100-------------------------- 
     101== The design: implementation == 
    81102 
    82 {{{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. 
     103These notes about the implementation are intended for GHC hackers, and logically form part of the GHC Commentary. 
    83104 
    84 [illissius] I checked thesaurus.com for (even remotely) plausible names, and this is what I found: 
    85  * Fact, Knowledge, Information, Data, Evidence, Proof 
    86  * Requirement, Constraint, Guarantee, Promise, Contract 
    87  * Characteristic, Attribute, Property, Trait, Capability 
    88  * Axiom, Lemma, Theorem, Proposition, Postulate, Premise, Claim, Posit 
     105A major change is that the data type `Type` (in module `TypeRep`) no longer has 
     106a `PredTy` construct.  Instead, we have just `Type`: 
    89107 
    90 [JonasDuregard] What about Context? That is after all the "official" name for the collections of constraints that appear in type signatures. 
    91     [illissius] I like it. 
     108 * In a function type `t1 -> t2`, the arguent `t1` is a ''constraint argument'' iff `t1 :: Constraint`. 
     109 
     110 * Constraint arguments are pretty-printed before a double arrow "`=>`" when displaying types.  Moreover they are passed implicitly in source code; for exmaple if `f :: ty1 => ty2 -> ty3` then the Haskell programmer writes a call `(f e2)`, where `e2 :: ty2`, and the compiler fills in the first argument of type `ty1`. 
     111 
     112 * A constraint type (of kind `Constraint`) can take one of these forms 
     113   * '''Equality constraint''': `TyConApp eqTyCon [ty1, ty2]`  
     114   * '''Class constraint''': `TyConApp tc [ty1, ty2]`, where `tc` is a `TyCon` whose `classTyCon_maybe` is `Just cls`. 
     115   * '''Implicit parameter''': `TyConApp tc [ty1]`, where `tc` is a `TyCon` whose `tyConIP_maybe` is `Just ip`. 
     116   * '''Constraint variable''': `TyVarTy tv` where `tv` has kind `Constraint`. 
     117   * '''Tuple constraint''': `TyConApp tup_tc [ty1, ..., tyn]`, where `tup_tc` is a constraint tuple `TyCon`.   
     118 
     119 * Implicit parameters have a type written `?x::Int`, say.  Concretely, this is represented as `TyConApp ?x [intTy]`, where `intTy` is the representation of the type for `Int`, and `?x` is a `TyCon` of kind `(* -> *)`.  There is an infinite family of such implicit-parameter `TyCon`s; see data constructor `IPTyCon` in data type `TyConParent` in `TyCon`. 
     120 
     121 * Constraint types (ie types with kind `Constraint`) are always boxed, including equality constraints.  So `(a ~ b)` is a ''boxed'' value.   We also have a primtive type of ''unboxed'' equality constraints, written `(a ~# b)`.  Roughly the former is declared thus: 
     122{{{ 
     123data a ~ b = Eq# (a ~# b) 
     124}}} 
     125 where `Eq#` is a data constructor with a single, unboxed, zero-width field of type `(a ~# b)`.  See `TysWiredIn.eqTyCon`. 
     126 
     127 * The constraint solver in the type checker deals solely in terms of boxed constraints. 
     128 
     129  * Constraint tup