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
- 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 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
.
Inhabitant KindStar val |