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 | |
| 30 | Having 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 | |