-- | Emulation of type-level functions.
module Data.TypeFun (

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

    -- * Construction of type-level functions
    Id (Id),
    Const (Const),
    (:->) ((:->)),
    FunMap,

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

) where

    import Data.Kind as Kind

    {-NOTE:
        At the value level, type-level function representations contain other /representations/ but
        nothing else.
    -}

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

    -- * Construction of 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

    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 -> ('App' /f/ arg -> 'App'
        /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

    {-|
        If @/t/@ is a type of kind @* -> *@, and @/f/@ is the representation of a
        type-level function, @FunMap /t/ /f/@ represents the function @\\arg -> /t/ (App /f/ arg)@.
    -}
    data FunMap (trans :: * -> *) fun = FunMap fun

    instance (TypeFun fun) => TypeFun (FunMap trans fun) where

        type Domain (FunMap trans fun) = Domain fun

    type instance App (FunMap trans fun) arg = trans (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