Version 7 (modified by dreixel, 5 years ago) (diff) |
---|

# Syntax for explicit type and kind application

As a replacement for lexically-scoped type variables (and pattern signatures),
we want to have syntax for explicit type (and kind) application. We propose
to use the syntax `@ tyvar` for this, like in the following example:

case x of (C @a y z) -> ....

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; 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:

case x of p@(C @a y z) -> ....

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:

id @Int 2

The idea is to provide more access to the explicit types in the core language (system FC-pro) 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:

f (C @_ @b x ) = ...

If the user gave a type signature for the binding, it is very easy to see which type patterns relate to which variables in the signature. In the absence 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.

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

### Ambiguity

Consider a problematic example:

f :: Int -> forall a. a f n @a = ....

In this case it is really ambiguous what the pattern means. For these cases we have the following workaround:

f :: Int -> forall a. a (f n) @a = ....

This approach should work in general, and hopefully only few programs will 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:

data X = X f :: forall (a : k). .... ... = ... f @'Nat @Nat ...

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 able to disambiguate between datatypes and their corresponding promoted kinds.

## More examples

### Impredicative instantiation

`Cons @(forall a. a -> a)` should mean 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:

type Typeable1 = Typeable @(* -> *)