Data.Kind

Support for subkinds, including subkind polymorphism.

Imagine, we had a language extension for declaring subkinds 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 an empty type KindK that represents 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
     
    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

Documentation

class Kind kind where

The class of subkind representations.

Associated Types

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

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.

Methods

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

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

class Kind kind => Inhabitant kind inhabitant where

Specifies what types are inhabitants of what subkinds.

Methods

specialize :: All kind item -> item inhabitant

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.