kinds-0.0.0.0: src/Data/Kind.hs

{-|
    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 @Kind/K/@ that
    represents the subkind. Then we add the following instance declaration:

    @
    instance Kind Kind/K/ where
     
        data All Kind/K/ item = All/K/ (forall /A_1/. /C_1/ => item /t_1/)
                                   ...
                                   (forall /A_n/. /C_n/ => item /t_n/)
     
        closed item = All/K/ 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 Kind/K/ /t_i/ where
     
        specialize (All/K/ _ ... _ 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
    @
-}
module Data.Kind (

    Kind (type All, closed),
    Inhabitant (specialize)

) where

    -- |The class of subkind representations.
    class Kind kind where

        {-|
            Universal quantification over the types of the subkind.

            For a subkind representation @Kind/K/@ of a subkind @/K/@ and a type @/f/@ of
            kind @* -> *@, @All Kind/K/ /f/@ is isomorphic to @forall a :: /K/. /f/ a@.
        -}
        data All kind :: (* -> *) -> *

        {-|
            Conversion from a type that uses normal universal quantification into one that uses
            subkind-specific universal quantification.
        -}
        closed :: (forall inhabitant. (Inhabitant kind inhabitant) => item inhabitant) ->
                  All kind item

    -- |Specifies what types are inhabitants of what subkinds.
    class (Kind kind) => Inhabitant kind inhabitant where

        {-|
            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@.
        -}
        specialize :: All kind item -> item inhabitant