|
|
# Syntax for explicit type and kind application
|
|
|
|
|
|
|
|
|
As a replacement for lexically-scoped type variables (and pattern signatures),
|
|
|
we want to have explicit type (and kind) application, like in the following
|
|
|
example:
|
|
|
We propose a replacement and generalisation of [lexically-scoped type variables](http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#scoped-type-variables) (and pattern signatures) that is
|
|
|
more clear and direct by allowing explicit type (and kind) application.
|
|
|
We propose the concrete syntax `@ tyvar`, like in the following example:
|
|
|
|
|
|
```wiki
|
|
|
case x of
|
... | ... | @@ -11,10 +11,11 @@ case x of |
|
|
```
|
|
|
|
|
|
|
|
|
On the right-hand side we would have the type variable `a` in scope.
|
|
|
On the right-hand side we would have the type variable `a` in scope for use on
|
|
|
any type signatures.
|
|
|
|
|
|
|
|
|
Note how the use of the symbol `@` is (in this case) unproblematic, since we can
|
|
|
Note how the use of the symbol `@` is (in this case) unproblematic; we can
|
|
|
use the fact that constructors always start with an uppercase letter to distinguish
|
|
|
whether the `@` refers to an "as pattern" or to a type application:
|
|
|
|
... | ... | @@ -24,14 +25,27 @@ case x of |
|
|
```
|
|
|
|
|
|
|
|
|
Also note that this would not allow you to to pattern-match on specific types:
|
|
|
the only thing that we can match on are type or kind variables.
|
|
|
Unfortunately this is not always the case; see below.
|
|
|
|
|
|
|
|
|
Note that this proposal would not allow pattern matching on specific types:
|
|
|
the only thing that we can match on are type or kind variables. However, it
|
|
|
does allow for specifying what type to apply:
|
|
|
|
|
|
```wiki
|
|
|
id @Int 2
|
|
|
```
|
|
|
|
|
|
|
|
|
The idea is to provide access to the explicit types in the core language
|
|
|
(system [ FC-pro](http://dreixel.net/research/pdf/ghp.pdf))
|
|
|
directly from the source language syntax.
|
|
|
|
|
|
## How many arguments, and their order
|
|
|
|
|
|
|
|
|
When we have multiple variables, we can use as many as we need, and also use
|
|
|
underscores:
|
|
|
When we have multiple variables we can pattern match on as many as we need,
|
|
|
and also use underscores:
|
|
|
|
|
|
```wiki
|
|
|
f (C @_ @b x ) = ...
|
... | ... | @@ -44,16 +58,14 @@ of a signature, though, there are two possible choices: |
|
|
|
|
|
- Reject matching on type variables altogether.
|
|
|
|
|
|
- Take the inferred signature, look at the introduced variables
|
|
|
|
|
|
|
|
|
syntactically from left to right, and use that order. This approach
|
|
|
does not require tracking which bindings were given type
|
|
|
signatures or not.
|
|
|
- Take the inferred signature, look at the introduced variables syntactically
|
|
|
from left to right, and use that order. This approach does not require tracking
|
|
|
which bindings were given type signatures or not.
|
|
|
|
|
|
|
|
|
A problem with taking the inferred signature is that it is tied to
|
|
|
many assumptions, including that of principal types.
|
|
|
\[Dimitrios: Can you expand on this?\]
|
|
|
|
|
|
## Parsing matters
|
|
|
|
... | ... | @@ -69,7 +81,7 @@ f n @a = .... |
|
|
|
|
|
|
|
|
In this case it is really ambiguous what the pattern means. For these
|
|
|
cases we have the following workaround:
|
|
|
cases we suggest the following workaround:
|
|
|
|
|
|
```wiki
|
|
|
f :: Int -> forall a. a
|
... | ... | @@ -83,8 +95,9 @@ actually need to use it. |
|
|
### Syntax for promoted datatypes
|
|
|
|
|
|
|
|
|
It also introduces the need to disambiguate between a datatype and its promoted
|
|
|
kind. Consider the example:
|
|
|
With `-XPolyKinds` on, we can also match/apply kind arguments. This introduces the
|
|
|
need to disambiguate between a datatype and the promoted kind it introduces.
|
|
|
Consider the example:
|
|
|
|
|
|
```wiki
|
|
|
data X = X
|
... | ... | @@ -95,21 +108,27 @@ f :: forall (a : k). .... |
|
|
|
|
|
|
|
|
Since now it is not clear from the context anymore if we are expecting a kind
|
|
|
or a type (since we use \|@\| both for kind and type application), we need to be
|
|
|
or a type (since we want to use `@` both for kind and type application), we need to be
|
|
|
able to disambiguate between datatypes and their corresponding promoted kinds.
|
|
|
At the moment this ambiguity does not arise, so we do not allow prefixing
|
|
|
kinds with `'`, but it seems natural to lift this restriction, and use the
|
|
|
same notation as for promoted data constructors.
|
|
|
|
|
|
## More examples
|
|
|
|
|
|
### Impredicative instantiation
|
|
|
|
|
|
`Cons @(forall a. a -> a)` should mean the constructor of type
|
|
|
|
|
|
This extension also allows for clear impredicative instantiation. For instance,
|
|
|
the application of the list constructor `(:) @(forall a. a -> a)` means
|
|
|
the constructor of type
|
|
|
`(forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a]`.
|
|
|
|
|
|
### Type/kind instantiation in classes
|
|
|
|
|
|
|
|
|
With the new kind-polymorphic `Typeable` class, we can recover the old
|
|
|
kind-specific classes by saying, for instance:
|
|
|
kind-specific classes by writing, for example:
|
|
|
|
|
|
```wiki
|
|
|
type Typeable1 = Typeable @(* -> *)
|
... | ... | |