Version 4 (modified by 6 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' -- We are a little unsure about this. Mabye we -- should kind-generalise 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 f8 :: forall k. forall 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

Rules:

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

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

#### Type classes

Additionnal rules:

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

in the signature is brought into scope

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

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'

#### Type families

Last rule becomes: Any missing kind signature defaults to `*`

-- Note (nothing to do with kind polymorphism): we might want to say that only the Bool is an index. type family F1 (b :: Bool) (true :: k) (false :: k) :: k -- F1 :: forall k. Bool -> k -> k -> k type family F2 b true false -- F2 :: * -> * -> * -> * type family F3 b (true :: k) false -- F3 :: forall k. * -> k -> * -> *

For type families it just doesn't make any sense to not write the whole kind signature, since there is no inference at all.

#### Type synonyms

type S1 f g -- (* -> *) -> (* -> *) -> * = forall a. f (g a) -- = forall (a :: *). f (g a) type S2 (f :: k1 -> *) g -- forall k1. (k1 -> *) -> (* -> k1) -> * = forall a. f (g a) -- = forall (a :: *). f (g a) type S3 (f :: k1 -> *) (g :: k2 -> k1) -- forall k1 k2. (k1 -> *) -> (k2 -> k1) -> * = forall a. f (g a) -- = forall (a :: k2). f (g a) type S4 f (g :: k2 -> k1) -- forall k1 k2. (k1 -> *) -> (k2 -> k1) -> * = forall a. f (g a) -- = forall (a :: k2). f (g a)