Design of Kind Polymorphism
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
*
-
A kind variable mentioned explicitly in a type must always be bound by an explicit
forall
, unlike type variables for which Haskell adds an implicitforall
. -
When there is no explicit
forall
, 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
- We kind generalize flexi meta kind variables when possible
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
foo1 :: f (g a) -> (f :: k1 -> *) b -- forall (a :: k2) (b :: k1). f (g a) -> f b
-- Note that k1 and k2 scope over the type signatures
-- just as f and g do.
class C2 f g where -- Same as C1
foo2 :: f (g a) -> f b -- Same as foo1
class C3 (f :: k1 -> *) g where -- Same as C1
foo3 :: f (g a) -> f b -- Same as foo1
Data types
data T1 s as where -- forall k. (k -> *) -> [k] -> *
Foo1 :: s a -> T1 s as -> T1 s (a ': as) -- forall k (s :: k -> *) (a :: k) (as :: [k]).
-- s a -> T1 k s as -> T1 k s ((':) k a as)
-- Note that s,a do not scope over the declaration of Foo1
data T2 s (as :: [k]) where -- Same as T1
Foo2 : s a -> T1 s as -> T1 s (a ': as) -- Same as Foo1
-- Note that s,as,k do not scope over the declaration of Foo2
data T3 s (as :: [*]) where -- (* -> *) -> [*] -> *
Foo3 : s a -> T1 s as -> T1 s (a ': as) -- forall (s :: * -> *) (a :: *) (as :: [*]).
-- s a -> T1 s as -> T1 s ((':) * a as)
-- Note that s,as do not scope over the declaration of Foo2
Type families
Last rule becomes: Any missing kind signature defaults to *
-- Note (nothing to do with kind polymorphism) that 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 k1 k2. (k1 -> *) -> (k2 -> k1) -> *
= forall a. f (g a) -- = forall (a :: k2). f (g a)
type S2 (f :: k1 -> *) g -- Same as S1
= forall a. f (g a) -- Same as S1
type S3 (f :: k1 -> *) (g :: k2 -> k1) -- Same as S1
= forall a. f (g a) -- Same as S1
type S4 f (g :: * -> *) -- (* -> *) -> (* -> *) -> *
= forall a. f (g a) -- = forall (a :: *). f (g a)