Version 3 (modified by dreixel, 2 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

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:

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.

How many arguments, and their order

When we have multiple variables, we can use as many as we need, and also use underscores:



  • Reject matching on type variables altogether.
  • Take the inferred signature, look at the introduced variables



Parsing matters


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 = ....


Syntax for promoted datatypes

It also introduces the need to disambiguate between a datatype and its promoted kind. Consider the example:

data X = X


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 @(* -> *)