Changes between Version 9 and Version 10 of DependentHaskell


Ignore:
Timestamp:
May 27, 2014 2:38:50 PM (14 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • DependentHaskell

    v9 v10  
    2323|| `=>` || no || solving || yes || yes ||
    2424
    25 * ''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 `->`!)
    26 * ''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. If something is visible, we must specify how it is parsed, noting that the term- and type-level parsers are different.
    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.
     25 Dependent::
     26  ''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 `->`!)
     27 Visible::
     28  ''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. If something is visible, we must specify how it is parsed, noting that the term- and type-level parsers are different.
     29 Required::
     30  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.
     31 Relevant::
     32  ''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.
    2933
    3034Having explained our terms with the current Haskell, the proposed set of quantifiers for dependent Haskell is below:
     
    4246
    4347The new `pi` quantifiers allow for quantifiees that are both dependent and relevant. This means that the quantifiee is named in the type and can be used within its scope in the type, and also that the quantifiee can be inspected in the term. A `pi`-bound argument is a proper dependent type. Since a `pi`-quantifiee can appear in both terms and types, its instantiations must come from a restricted subset of Haskell that makes sense at both the type and term level. This issue is addressed in [#gundry Adam Gundry's thesis]. For now, we propose that this subset include only data constructors (perhaps applied) and other `pi`-quantifiees. The subset can be expanded later. For some tantalizing ideas of how far it can go, see [#promotion this paper], discussing promotion of Haskell terms to types.
     48
     49The table above has a new abbreviation: ''Rel.I.'' is short for ''relevance inference''. When a type variable is used in a type without an explicit quantification, should it be `forall`-quantified or `pi`-quantified? Choosing `forall` quantification means that the type can be erased during compilation, while `pi` quantification is more powerful. Thus, we can't just have a default. We must infer the relevance of the type variable, by looking at its use sites. This seems actually quite straightforward, and is remarkably similar to role inference. (Indeed, the phantom role seems to correspond quite closely to an irrelevant argument. There is Something Interesting here -- yet another way that roles and parametricity relate.)
     50
     51It is tempting to treat `->` as a degenerate form of a `pi` -- something like `pi (_ :: ...) ->`. However, this is slightly misleading, in that `->` quantifies over ''any'' Haskell term, and `pi` quantifies over only the shared term/type subset.
     52
     53=== Quantifiers in kinds ===
     54
     55The preceding discussion focuses mostly on classifying terms. How does any of this change when we think of classifying types?
     56
     57 Relevance in types::
     58  Relevance in a term corresponds quite closely to phase. A relevant term-level quantifiee must be kept at runtime, while an irrelevant quantifiee can be erased. But, what does relevance in a type mean? Everything in a type is (absent `pi`-quantifications) irrelevant in a term, and it all can be erased. Furthermore, it is all used in the same phase, at compile time. Yet, it seems useful to still have a notion of relevance in types. This allows programmers to reason about parametricity in their type-level functions, and it keeps the function space in types similar to the function space in terms.
     59
     60  For example, today's Haskell permits things like this:
     61  {{{
     62  type family F (x :: k) :: k
     63  type instance F True = False
     64  type instance F False = True
     65  type instance F (x :: *) = x
     66  }}}
     67
     68  Note that the behavior of `F` depends on the ''kind'' of its argument, `k`. This is an example of a non-parametric type function. Looking at the kind, `k -> k`, one would expect `F` to be the identity; yet, it is not.
    4469
    4570== Open design questions ==