kinds-0.0.1.1: src/Data/Kind.hs

{-|
    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 @Kind/K/@ with a nullary data
    constructor of the same name for representing 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 = 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 (

    -- * Subkinds in general
    Kind (type All, closed),
    Inhabitant (specialize),

    -- * Kind @*@ as a subkind of itself
    KindStar (KindStar)

) where

    -- * Subkinds in general
    -- |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 val :: /K/. /f/ val@.
        -}
        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

    -- * Kind @*@ as a subkind of itself
    -- |Represents kind @*@ itself.
    data KindStar = KindStar

    instance Kind KindStar where

        data All KindStar item = AllStar (forall val. item val)

        closed item = AllStar item

    instance Inhabitant KindStar val where

        specialize (AllStar item) = item