Support for subkinds of kind `*`

, including subkind polymorphism.

Imagine, we had a language extension for declaring subkinds of kind `*`

where a subkind
declaration would be written as follows:

subkindK=C_1=>t_1| ... |C_n=>t_n

Thereby,

would be a kind identifier, the *K*

would be types and the *t_i*

would
be contexts. This subkind declaration would introduce a subkind *C_i*

that covers all types
that match one of the *K*

and fulfill the corresponding context. For example, the
declaration
*t_i*

subkind Map = (Ord key) => Map key val | IntMap val

would declare the subkind `Map`

of all types whose values are maps. Note that the subkind `Map`

would be different from the type `Map`

.

We will now see how a subkind declaration

subkindK=C_1=>t_1| ... |C_n=>t_n

can be emulated using this module. First, we declare a type `Kind`

with a nullary data
constructor of the same name for representing the subkind. Then we add the following instance
declaration:
*K*

instance Kind KindKwhere data All KindKitem = AllK(forallA_1.C_1=> itemt_1) ... (forallA_n.C_n=> itemt_n) closed item = AllKitem ... item

Thereby, each

stands for a whitespace-separated sequence of the free variables
of *A_i*

. Finally, we add the following instance declaration for every *t_i*

between
*i*`1`

and

:
*n*

instanceC_i=> Inhabitant KindKt_iwhere specialize (AllK_ ... _ item _ ... _) = item

Thereby, the number of wildcard patterns before and after `item`

is

and *i* - 1

,
respectively. The above subkind declaration for *n* - *i*`Map`

can be emulated with the following code:

data KindMap = KindMap instance Kind KindMap where data All KindMap item = AllMap (forall key val. (Ord key) => item (Map key val)) (forall val. item (IntMap val)) closed item = AllMap item item instance (Ord key) => Inhabitant KindMap (Map key val) where specialize (AllMap item _) = item instance Inhabitant KindMap (IntMap val) where specialize (AllMap _ item) = item

- class Kind kind where
- data All kind :: (* -> *) -> *
- closed :: (forall inhabitant. Inhabitant kind inhabitant => item inhabitant) -> All kind item

- class Kind kind => Inhabitant kind inhabitant where
- specialize :: All kind item -> item inhabitant

- data KindStar = KindStar

# Subkinds in general

The class of subkind representations.

data All kind :: (* -> *) -> *Source

Universal quantification over the types of the subkind.

For a subkind representation `Kind`

of a subkind *K*

and a type *K*

of
kind *f*`* -> *`

, `All Kind`

is isomorphic to *K* *f*`forall val :: `

.
*K*. *f* val

closed :: (forall inhabitant. Inhabitant kind inhabitant => item inhabitant) -> All kind itemSource

Conversion from a type that uses normal universal quantification into one that uses subkind-specific universal quantification.

class Kind kind => Inhabitant kind inhabitant whereSource

Specifies what types are inhabitants of what subkinds.

specialize :: All kind item -> item inhabitantSource

Conversion from a universally quantified type into a type that is fixed to a specific inhabitant.

This method exists to ensure that one cannot extend the subkind. If one would try to add
a new inhabitant, one would have to provide an implementation of `specialize`

.

Inhabitant KindStar val |