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

## Design of Kind Polymorphism

This is a simple proposal, that would allow us to do better later, but still allow us to go on step 3.

Implicit foralls are added by the renamer. Kind generalization (adding more kind foralls) is done by the type checker.

### In types

Rules:

- When there is an explicit forall, we don't add any foralls, which means:
- no implicit foralls even for kind variables
- no kind generalization, which means defaulting flexi meta kind variables to
`*`

- When there is no explicit foralls, we add an implicit forall for not-in-scope
*type*variables in the renamer and we kind generalize in the type checker - In the context of a function signature, an explicit forall binds its variables (type or kind) in the function equations (as it is currently the case for type variables).

-- For the following examples, no type or kind variables are in scope f1 :: f a -> Int -- forall k (f :: k -> *) (a :: k). f a -> Int f2 :: f (a :: k) -> Int -- Not in scope: kind variable `k' f3 :: forall a. f a -> Int -- Not in scope: type variable `f' f4 :: forall f a. f a -> Int -- forall (f :: * -> *) (a :: *). f a -> Int f5 :: forall f (a :: k). f a -> Int -- Not in scope: kind variable `k' f6 :: forall k f a. f a -> Int -- Warning: Unused quantified type variable `k' -- forall k (f :: * -> *) (a :: *). f a -> Int f7 :: forall k f (a :: k). f a -> Int -- forall k (f :: k -> *) (a :: k). f a -> Int g1 :: (f a -> Int) -> Int -- forall (f :: k -> *) (a :: k). (f a -> Int) -> Int g2 :: (forall f a. f a -> Int) -> Int -- forall k. (forall (f :: k -> *) (a :: k). f a -> Int) -> Int g3 :: (forall a. f a -> Int) -> Int -- forall k (f :: k -> *). (forall (a :: k). f a -> Int) -> Int g4 :: forall f. (forall a. f a -> Int) -> Int -- forall (f :: * -> *). (forall (a :: *). f a -> Int) -> Int g5 :: (forall f (a :: k). f a -> Int) -> Int -- Not in scope: kind variable `k' h :: forall k f (a :: k). f a -> Int h x = ...k...f a... -- k, f, and a are in scope

### In kinds

The story is more complicated since we have several ways of talking about kinds: data types, type classes, type families, and type synonyms.

We need a notion of large scoping, which means that a variable in the signature can bind in the where clause.

#### Type classes

Rules:

- Large scoping: any type or kind variables appearing on left or right side of a
`::`

in the signature is brought into scope - Any explicit kind variables are generalized over
- Defaulting for flexi meta kind variables

class C1 (f :: k1 -> *) (g :: k2 -> k1) where -- forall k1 k2. (k1 -> *) -> (k2 -> k1) -> Constraint foo :: f (g a) -> f b -- forall (a :: k2) (b :: k1). f (g a) -> f b -- C2 looks much easier with defaulting class C2 f g where -- (* -> *) -> (* -> *) -> Constraint foo :: f (g a) -> f b -- forall (a :: *) (b :: *). f (g a) -> f b class C3 (f :: k1 -> *) g where -- forall k1. (k1 -> *) -> (* -> k1) -> Constraint foo :: f (g a) -> f b -- forall (a :: k1) (b :: *) -> f (g a) -> f b

#### Data types

Rules:

- No large scoping
- Any explicit kind variables are generalized over
- Defaulting for flexi meta kind variables

data T1 s as where -- (* -> *) -> [*] -> * Foo :: s a -> T1 s as -> T1 s (a ': as) -- forall (s :: * -> *) (a :: *) (as :: [*]). the same data T1 s (as :: [k]) where -- forall k. (k -> *) -> [k] -> * Foo : s a -> T1 s as -> T1 s (a ': as) -- forall k (s :: k -> *) (a :: k) (as :: [k]). the same where `T1' becomes `T1 k'