kinds- Emulation of subkinds and subkind polymorphism




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:

    subkind K = C_1 => t_1 | ... | C_n => t_n

Thereby, K would be a kind identifier, the t_i would be types and the C_i would be contexts. This subkind declaration would introduce a subkind K that covers all types that match one of the t_i and fulfill the corresponding context. For example, the declaration

    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

    subkind K = C_1 => t_1 | ... | C_n => t_n

can be emulated using this module. First, we declare a type KindK with a nullary data constructor of the same name for representing the subkind. Then we add the following instance declaration:

    instance Kind KindK where
        data All KindK item = AllK (forall A_1. C_1 => item t_1)
                                   (forall A_n. C_n => item t_n)
        closed item = AllK item ... item

Thereby, each A_i stands for a whitespace-separated sequence of the free variables of t_i. Finally, we add the following instance declaration for every i between 1 and n:

    instance C_i => Inhabitant KindK t_i where
        specialize (AllK _ ... _ item _ ... _) = item

Thereby, the number of wildcard patterns before and after item is i - 1 and n - i, respectively. The above subkind declaration for 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


Subkinds in general

class Kind kind whereSource

The class of subkind representations.

Associated Types

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

Universal quantification over the types of the subkind.

For a subkind representation KindK of a subkind K and a type f of kind * -> *, All KindK f is isomorphic to forall a :: K. f a.


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.


Kind * as a subkind of itself

data KindStar Source

Represents kind * itself.