module Data.TypeFun (

    -- * Type-level functions in general
    TypeFun (type Domain),
    App,

    -- * Specific type-level functions
    Id (Id),
    Const (Const),
    (:->) ((:->)),

    -- * Utilities
    WrappedApp (WrapApp),
    unwrapApp,
    Universal

) where

    import Data.Kind as Kind

    -- * Type-level functions in general
    {-|
        Type-level functions are represented by types. @TypeFun@ is the class of all type-level
        function representations.
    -}
    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

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

    -- * Specific type-level functions
    infixr 1 :->

    {-|
        A type @Id /d/@ represents the type-level identity function whose domain is represented
        by /d/.
    -}
    data Id dom = 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 = 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

    {-|
        A type @/f/ :-> /f'/@ represents the type-level function @\\arg -> (/f/ arg -> /f'/ arg)@.
    -}
    data fun :-> fun' = fun :-> 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

    -- * Utilities
    -- |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