... | ... | @@ -163,11 +163,17 @@ The preceding discussion focuses mostly on classifying terms. How does any of th |
|
|
>
|
|
|
> Thus, we would want to distinguish `pi k. k -> k` (the kind of `F`) and `forall k. k -> k` (the kind of a type-level polymorphic identity). This distinction does not affect erasure or phase, but it does affect how a quantifiee can be used. Furthermore, this keeps term classifiers more in line with type classifiers. Note that this means all current type/data families are properly classified with `pi`, not `forall`. This won't cause code breakage, though, because it is impossible to write a kind quantification (with any syntax) in today's Haskell.
|
|
|
|
|
|
>
|
|
|
> Proposed syntax for this distinction is to assume any kind variable is forall-quantified, and allow syntax like `type family pi k. F (x :: k) :: k where ...` to get pi-quantification. `forall` would be allowed in that syntax as well, but would be redundant.
|
|
|
|
|
|
<table><tr><th>Datatypes</th>
|
|
|
<td>
|
|
|
How is the kind of a datatype classified? After some debate, Stephanie and RAE thought that a poly-kinded datatype should be quantified with `pi`, not `forall`. For example, consider `data Proxy (k :: *) (a :: k) = Proxy`. Is its kind `forall (k :: *). k -> *` or `pi (k :: *). k -> *`. Let's consider the former type as if it classified a term-level function. That function would have to be a constant function, by parametricity. Yet, we do *not* want `Proxy * Bool` to be the same as `Proxy Nat Zero`. So, we choose the latter classifier. For now, we don't see the need to introduce a way for programmers to declare datatypes classified by `forall`, but there doesn't seem to be anything broken by allowing such an extension.
|
|
|
How is the kind of a datatype classified? After some debate, Stephanie and RAE thought that a poly-kinded datatype should be quantified with `pi`, not `forall`. For example, consider `data Proxy (k :: *) (a :: k) = Proxy`. Is its kind `forall (k :: *). k -> *` or `pi (k :: *). k -> *`. Let's consider the former type as if it classified a term-level function. That function would have to be a constant function, by parametricity. Yet, we do *not* want `Proxy * Bool` to be the same as `Proxy Nat Zero`. So, we choose the latter classifier.
|
|
|
</td></tr></table>
|
|
|
|
|
|
>
|
|
|
> This choice matters in how datatypes are used in pattern-matching situations. For example, is this possible: `type instance F (Proxy (a :: k)) = k`? The result uses `k` in a relevant context, so it must be that `k` is introduced in a relevant context, and thus that it must be pi-quantified. If we wanted to introduce forall-quantification in datatypes, then the use of these variables would be restricted during matching. Is this a good idea? Is this necessary? And, it seems that `pi` will be default in datatypes but `forall` will be default in type families. This is strange.
|
|
|
|
|
|
## Open design questions
|
|
|
|
|
|
### Parsing/namespace resolution
|
... | ... | @@ -236,7 +242,15 @@ The `.`/`->` distinction in quantifiers allows programmers to specify the visibi |
|
|
|
|
|
### Parametric vs. Non-parametric type families
|
|
|
|
|
|
- We must have a concrete syntax to declare both of these sorts of type and data families. There are no current proposals for this.
|
|
|
- How does relevance inference work with the proposed syntax for quantifier choice in type families? For example:
|
|
|
|
|
|
```wiki
|
|
|
type family X (a :: k) :: * where
|
|
|
X (a :: k) = k
|
|
|
```
|
|
|
|
|
|
|
|
|
Because, in the equation, `k` appears in a relevant context within the result, it must be pi-quantified. Yet, we said above that kind variables without explicit quantification would default to `forall`. What to do here?
|
|
|
|
|
|
# Type Inference
|
|
|
|
... | ... | |