-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Emulation of type-level functions
--   
--   This package supports emulation of type-level functions using
--   defunctionalization. All functions whose domain is a subkind of
--   <tt>*</tt> and whose codomain is <tt>*</tt> itself can be represented.
--   
--   For detailed information, please refer to Subsection 3.2 of the paper
--   <i>Generic Record Combinators with Static Type Checking</i>.
@package type-functions
@version 0.2.0.4


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

-- | Type-level functions are represented by types. <tt>TypeFun</tt> is the
--   class of all type-level function representations.
class (Kind (Domain fun)) => TypeFun fun where type Domain fun where {
    type family Domain fun;
}

-- | Application of type-level functions. <tt>App</tt> takes a function
--   representation and an argument and returns the corresponding result.

-- | A type <tt>Id <i>d</i></tt> represents the type-level identity
--   function whose domain is represented by <tt><i>d</i></tt>.
data Id dom
Id :: dom -> Id dom

-- | A type <tt>Const <i>d</i> <i>v</i></tt> represents the constant
--   type-level function whose domain is represented by <tt><i>d</i></tt>,
--   and whose result is <tt><i>v</i></tt>.
data Const dom val
Const :: dom -> Const dom val

-- | A type <tt><i>f</i> :-&gt; <i>f'</i></tt> represents the type-level
--   function <tt>\arg -&gt; (<a>App</a> <i>f</i> arg -&gt; <a>App</a>
--   <i>f'</i> arg)</tt>.
data (:->) fun fun'
(:->) :: fun -> fun' -> (:->) fun fun'

-- | If <tt><i>t</i></tt> is a type of kind <tt>* -&gt; *</tt>, and
--   <tt><i>f</i></tt> is the representation of a type-level function,
--   <tt>FunMap <i>t</i> <i>f</i></tt> represents the function <tt>\arg
--   -&gt; <i>t</i> (App <i>f</i> arg)</tt>.
data FunMap (trans :: * -> *) fun

-- | A data type that is isomorphic to the type synonym family <a>App</a>.
newtype WrappedApp fun arg
WrapApp :: (App fun arg) -> WrappedApp fun arg

-- | The inverse of <a>WrapApp</a>.
unwrapApp :: WrappedApp fun arg -> App fun arg

-- | Turns a type-level function into the intersection of all its results.
type Universal fun = forall arg. (Inhabitant (Domain fun) arg) => WrappedApp fun arg
instance Data.Kind.Kind dom => Data.TypeFun.TypeFun (Data.TypeFun.Id dom)
instance Data.Kind.Kind dom => Data.TypeFun.TypeFun (Data.TypeFun.Const dom val)
instance (Data.TypeFun.TypeFun fun, Data.TypeFun.TypeFun fun', Data.TypeFun.Domain fun ~ Data.TypeFun.Domain fun') => Data.TypeFun.TypeFun (fun Data.TypeFun.:-> fun')
instance Data.TypeFun.TypeFun fun => Data.TypeFun.TypeFun (Data.TypeFun.FunMap trans fun)