... | @@ -5,18 +5,27 @@ As a replacement for lexically-scoped type variables (and pattern signatures), |
... | @@ -5,18 +5,27 @@ As a replacement for lexically-scoped type variables (and pattern signatures), |
|
we want to have explicit type (and kind) application, like in the following
|
|
we want to have explicit type (and kind) application, like in the following
|
|
example:
|
|
example:
|
|
|
|
|
|
|
|
```wiki
|
|
|
|
case x of
|
|
|
|
(C @a y z) -> ....
|
|
|
|
```
|
|
|
|
|
|
|
|
|
|
|
|
On the right-hand side we would have the type variable `a` in scope.
|
|
|
|
|
|
|
|
|
|
|
|
Note how the use of the symbol `@` is (in this case) unproblematic, since 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:
|
|
|
|
|
|
```wiki
|
|
```wiki
|
|
case x of
|
|
case x of
|
|
p@(C @a y z) -> ....
|
|
p@(C @a y z) -> ....
|
|
```
|
|
```
|
|
|
|
|
|
|
|
|
|
On the right-hand side we would have the type variable `a` in scope. Note how
|
|
Also note that this would not allow you to to pattern-match on specific types:
|
|
the use of `@` is (in this case) unproblematic, since we can use the fact that
|
|
the only thing that we can match on are type or kind variables.
|
|
constructors always start with an uppercase letter to distinguish whether the
|
|
|
|
`@` refers to an "as pattern" or to a type application. This cannot be used
|
|
|
|
to pattern-match on specific types: the only thing that we can match on are
|
|
|
|
variables.
|
|
|
|
|
|
|
|
## How many arguments, and their order
|
|
## How many arguments, and their order
|
|
|
|
|
... | | ... | |