module Data.TypeFun (

    TypeFun (type Domain),
    App,
    WrappedApp (WrapApp),
    unwrapApp,
    Universal,
    Id,
    Const

) where

    import Data.Kind as Kind

    {-|
        Type-level functions are represented by types. @TypeFun@ is the class of all function
        representations.

        Note that the @(->)@ instance of @TypeFun@ slightly abuses the type
        constructor @(->)@. In representations of type-level functions, @(->)@ denotes the
        lifting of the type constructor @(->)@. That is if @/r/@ and @/r'/@ are
        representations of functions @/f/@ and @/f'/@, the type @/r/ -> /r'/@ represents
        the function @\\t -> (/f/ t -> /f'/ t)@.
    -}
    class (Kind (Domain fun)) => TypeFun fun where

        {-|
            The domain of the type-level function as a subkind representation. Subkind handling is
            provided by the /kinds/ package.
        -}
        type Domain fun

    instance (TypeFun fun, TypeFun fun', Domain fun ~ Domain fun') => TypeFun (fun -> fun') where

        type Domain (fun -> fun') = Domain fun

    type instance App (fun -> fun') arg = App fun arg -> App fun' arg

    {-|
        Application of type-level functions. @App@ takes a function representation and an argument
        and returns the corresponding result.
    -}
    type family App fun arg

    -- |A data type that is isomorphic to the type synonym family 'App'.
    newtype WrappedApp fun arg = WrapApp (App fun arg)

    -- |The inverse of 'WrapApp'.
    unwrapApp :: WrappedApp fun arg -> App fun arg
    unwrapApp (WrapApp val) = val

    -- |Turns a type-level function into the intersection of all its results.
    type Universal fun = forall arg. (Inhabitant (Domain fun) arg) => WrappedApp fun arg

    {-|
        A type @Id /d/@ represents the type-level identity function whose domain is represented
        by /d/.
    -}
    data Id dom

    instance (Kind dom) => TypeFun (Id dom) where

        type Domain (Id dom) = dom

    type instance App (Id dom) arg = arg

    {-|
        A type @Const /d/ /v/@ represents the constant type-level function whose domain is
        represented by /d/, and whose result is @/v/@.
    -}
    data Const dom val

    instance (Kind dom) => TypeFun (Const dom val) where

        type Domain (Const dom val) = dom

    type instance App (Const dom val) arg = val