|
|
## 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
|
... | ... | @@ -11,7 +8,7 @@ Implicit foralls are added by the renamer. Kind generalization (adding more kind |
|
|
|
|
|
Rules:
|
|
|
|
|
|
- When there is an explicit forall, we don't add any foralls, which means:
|
|
|
- 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 `*`
|
... | ... | @@ -37,9 +34,11 @@ 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
|
|
|
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
|
... | ... | @@ -61,7 +60,7 @@ h x = ...k...f a... -- k, f, and a are in scope |
|
|
Rules:
|
|
|
|
|
|
- Any explicit kind variables are generalized over
|
|
|
- Defaulting for flexi meta kind variables
|
|
|
- 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.
|
... | ... | @@ -75,16 +74,15 @@ Additionnal rules: |
|
|
|
|
|
```wiki
|
|
|
class C1 (f :: k1 -> *) (g :: k2 -> k1) where -- forall k1 k2. (k1 -> *) -> (k2 -> k1) -> Constraint
|
|
|
foo :: f (g a) -> (f :: k1 -> *) b -- forall (a :: k2) (b :: k1). f (g a) -> f b
|
|
|
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.
|
|
|
|
|
|
-- 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 C2 f g where -- Same as C1
|
|
|
foo2 :: f (g a) -> f b -- Same as foo1
|
|
|
|
|
|
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
|
|
|
class C3 (f :: k1 -> *) g where -- Same as C1
|
|
|
foo3 :: f (g a) -> f b -- Same as foo1
|
|
|
```
|
|
|
|
|
|
#### Data types
|
... | ... | @@ -93,11 +91,16 @@ class C3 (f :: k1 -> *) g where -- forall k1. (k1 -> *) -> (* -> |
|
|
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 Foo
|
|
|
-- 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 Foo
|
|
|
-- 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
|
... | ... | @@ -106,7 +109,7 @@ data T2 s (as :: [k]) where -- Same as T1 |
|
|
Last rule becomes: Any missing kind signature defaults to `*`
|
|
|
|
|
|
```wiki
|
|
|
-- Note (nothing to do with kind polymorphism): we might want to say that only the Bool is an index.
|
|
|
-- 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 :: * -> * -> * -> *
|
... | ... | @@ -120,15 +123,15 @@ For type families it just doesn't make any sense to not write the whole kind sig |
|
|
#### Type synonyms
|
|
|
|
|
|
```wiki
|
|
|
type S1 f g -- (* -> *) -> (* -> *) -> *
|
|
|
= forall a. f (g a) -- = forall (a :: *). f (g a)
|
|
|
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 -- forall k1. (k1 -> *) -> (* -> k1) -> *
|
|
|
= forall a. f (g a) -- = forall (a :: *). 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) -- forall k1 k2. (k1 -> *) -> (k2 -> k1) -> *
|
|
|
= forall a. f (g a) -- = forall (a :: k2). f (g a)
|
|
|
type S3 (f :: k1 -> *) (g :: k2 -> k1) -- Same as S1
|
|
|
= forall a. f (g a) -- Same as S1
|
|
|
|
|
|
type S4 f (g :: k2 -> k1) -- forall k1 k2. (k1 -> *) -> (k2 -> k1) -> *
|
|
|
= forall a. f (g a) -- = forall (a :: k2). f (g a)
|
|
|
type S4 f (g :: * -> *) -- (* -> *) -> (* -> *) -> *
|
|
|
= forall a. f (g a) -- = forall (a :: *). f (g a)
|
|
|
``` |
|
|
\ No newline at end of file |