Changes between Version 6 and Version 7 of DependentHaskell


Ignore:
Timestamp:
May 27, 2014 1:04:46 PM (14 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • DependentHaskell

    v6 v7  
    66
    77It is possible to fix #7961 without any surface language changes, as that bug addresses only lifting restrictions on promotion. There is a chance that this bugfix will enter HEAD without all of the other features below, but this writeup generally will not consider fixing #7961 separate from adding dependent types.
     8
     9=== Merging Types and Kinds ===
     10
     11Following the work in [#nokinds the kind equality paper], the new Haskell will merge types and kinds into one syntactic and semantic category. Haskell will have the `* :: *` property. As a consequence, it will be easily possible to explicit quantify over kinds. In other words, the following type signature is allowed: `forall (k :: *) (a :: k). Proxy a -> Proxy a`. Furthermore, kind variables will be able to be listed explicitly when declaring datatypes and classes. Of course, if a kind variable is listed explicitly in the declaration of a type or class, then it also must be listed explicitly at the use sites. Note that this change will completely eliminate `BOX`.
    812
    913=== Quantifiers ===
     
    2125* ''Dependent'' means that the quantified thing (henceforth, ''quantifiee'') can appear later in the type. This is clearly true for `forall`-quantified things and clearly not true for `->`-quantified things. (That is, if we have `Int -> Bool`, we can't mention the `Int` value after the `->`!)
    2226* ''Visibility'' refers to whether or not the argument must appear at call sites in the program text. If something is not visible, the table lists how GHC is to fill in the missing bit at call sites.
    23 * A ''required'' quantification is one that must textually appear in the type. Note that Haskell freely infers the type `a -> a` really to mean `forall a. a -> a`, by looking for free variables (abbreviated to FVs, above).
    24 * ''Relevance'' refers to how the quantifiee can be used in the term that follows. (This is distinct from dependence, which says how the quantifiee can be used in the ''type'' that follows!) `forall`-quantifiees are not relevant. While they can textually appear in the term that follows, they appear only in irrelevant positions -- that is, in type annotations and type signatures. `->`- and `=>`-quantifiees, on the other hand, can be used freely.
    25 Relevance is something of a squirrely issue. It is (RAE believes) closely related to parametricity, in that if `forall`-quantifiees were relevant, Haskell would lose the parametricity property. Another way to think about this is that parametric arguments are irrelevant and non-parametric arguments are relevant.
     27* A ''required'' quantification is one that must textually appear in the type. Note that Haskell freely infers the type `a -> a` really to mean `forall a. a -> a`, by looking for free variables (abbreviated to FVs, above). Haskell currently does slightly more than analyze just free variables, though: it also quantifies over free ''kind'' variables that do not textually appear in a type. For example, the type `Proxy a -> Proxy a` really means (in today's Haskell) `forall (k :: BOX) (a :: k). Proxy a -> Proxy a`, even though `k` does not appear in the body of the type. Note that a ''visible'' quantifications impose a requirement on how a thing is used/written; ''required'' quantifications impose a requirement on how a thing's type is written.
     28* ''Relevance'' refers to how the quantifiee can be used in the term that follows. (This is distinct from dependence, which says how the quantifiee can be used in the ''type'' that follows!) `forall`-quantifiees are not relevant. While they can textually appear in the term that follows, they appear only in irrelevant positions -- that is, in type annotations and type signatures. `->`- and `=>`-quantifiees, on the other hand, can be used freely. Relevance is something of a squirrely issue. It is (RAE believes) closely related to parametricity, in that if `forall`-quantifiees were relevant, Haskell would lose the parametricity property. Another way to think about this is that parametric arguments are irrelevant and non-parametric arguments are relevant.
     29
     30Having explained our terms with the current Haskell, the proposed set of quantifiers for dependent Haskell is below:
     31
     32||||||||||  Dependent Haskell  ||
     33||= Quantifier =||= Dependent? =||= Visible? =||= Required? =||= Relevant? =||
     34|| `forall (...) .` || yes || unification || FVs + Rel.I. || no ||
     35|| `forall (...) ->` || yes || yes || yes || no ||
     36|| `pi (...) .` || yes || unification || FVs + Rel.I. || yes ||
     37|| `pi (...) ->` || yes || yes || yes || yes ||
     38|| `->` || no || yes || yes || yes ||
     39|| `=>` || no || solving || yes || yes ||
     40
    2641
    2742
     
    3348There are several published works very relevant to the design:
    3449
    35 * [http://www.cis.upenn.edu/~eir/papers/2013/fckinds/fckinds.pdf System FC with Explicit Kind Equality]. Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg. ICFP 2013.
     50* [http://www.cis.upenn.edu/~eir/papers/2013/fckinds/fckinds.pdf System FC with Explicit Kind Equality]. [=#nokinds Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg]. ICFP 2013.
    3651* [https://personal.cis.strath.ac.uk/adam.gundry/thesis/thesis-2013-07-24.pdf Type Inference, Haskell, and Dependent Types]. Adam Gundry. PhD Thesis, 2013.
    3752