Version 1 (modified by guest, 6 years ago) (diff) |
---|

# Polymorphic Kinds for Haskell

Currently thinking about adding **Polymorphic Kinds** to GHC...
(Currently very WIPish)

## Example: At the term level

f :: forall_kind k . forall (m :: k -> *) (a :: k) . m a -> Int f _ = 2 data T m = MkT (m Int) foo = f (Just 2) -- m = Maybe, a = Int bar = f (MkT (Just 2)) -- m = T , a = Maybe

## Example: Typeable[123..]

With polymorphic kinds, it should be possible to remove the need for
`Typeable[1,2,3,..]` classes from SYB for kinds that arn't `*`.

Because we need a way of talking about the types (and hence their kinds) in the type classes' functions, we will need a proxy data type:

data Proxy :: forall k . k -> * forall_kind k . class Typeable (t :: k) where typeOf :: Proxy t -> TypeRep instance Typeable Bool where typeOf _ = mkTyCon "Prelude.Bool" [] instance Typeable Maybe where typeOf _ = mkTyConApp (mkTyCon "Prelude.Mabe") [] instance Typeable Either where typeOf _ = ... instance (Typeable (t1 :: (* -> *), Typeable (t2 :: *))) => Typeable (t1 t2) where typeOf _ = (typeOf (undefined :: t1)) `mkAppTy` (typeOf (undefined :: t2))

## Functions Quantifying over Kinds

For function signatures, we need a way of quantifying over kinds. Options:

### Option 1: Add forall_kind (or equivt.) notation

As in the example above, functions would need a new quantifier to explicitly mark when a new kind is being quantified over.

If it were to take the form `forall_kind vars .` then it shouldn't interact
with existing forms.

### Option 2: Use forall and infer kind variables from usage

f :: forall k (m :: k -> *) (a :: k) . m a -> Int f _ = 2

In the above example, it is clear* that k must quantify over kinds as it appears in the kind signatures.

*=well...

** Pros: **

- No new syntax

** Cons: **

- More complicated for both users and implementaion logic to work out what's going on

### Option 3: Completely implicit quantified kind variables

f :: forall (m :: k -> *) (a :: k) . m a -> Int

**Pros:**

- In line with haskell type variables being implicitly quantified

** Cons: **

- This makes it hard to add additional constraints to the k in future (sort annotations, kind classes?)

- A typo with a rank-n kind could be very confusing, e.g.

f :: forall (m :: k -> (forall k . k' -> *))

## Type Classes

class Bar (a :: k -> *) where -- standalone class Bar (a :: k -> *) => Baz (a :: * -> k) where -- superclass, explicit name (shared) class Bar a => Baz (a :: * -> k) where -- superclass, implicit or new name? instance Bang (a :: k -> *) => Bar (a :: k -> *) -- instance implication, explic

class forall k . Blah (a :: k -> *) where

class forall k . Baz (a :: k -> *) => Bar (a :: * -> k) where

## Syntax of Kinds

kind ::= * | # | ? | (kind) | kind -> kind | ty :=: ty | forall var . kind | var

## Syntax of Types

Type syntax need to be extended with a new binder TODO

## Type Classes

TODO

## To classify

Other 'issues' (probably non-issues). Kinds in rank-n types? foobar :: forall k1 (b :: k1) (c :: k1 -> *) . (forall k2 (e :: k2 -> *) (f :: k) . e f -> Int ) -> b c -> Int

Impredicativity

data Proxy :: forall k . k -> * foo :: forall (m :: forall k . k -> *) . m Int -> m Maybe -> Int -- This is ok bar = foo Proxy Proxy

data Foo :: forall k . k -> * foo :: forall (m :: (forall k . k -> *) -> *) . m Proxy -> Int -- This line is ok -- has a higher -- ranked kind, but -- that's not an -- issue as we -- have to be -- explicit bar = foo Foo -- This is impredicative (and rejected) as it requires instantiating -- Foo's k to (forall k . k -> *)