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


-- | Utilities to work with lists of types
--   
--   This packages reifies the concept of list of types, and application of
--   those to list constructors.
@package kind-apply
@version 0.3.0.0

module Data.PolyKinded

-- | <tt>LoT k</tt> represents a list of types which can be applied to a
--   data type of kind <tt>k</tt>.
data LoT k

-- | Empty list of types.
[LoT0] :: LoT *

-- | Cons a type with a list of types.
[:&&:] :: k -> LoT ks -> LoT (k -> ks)
infixr 5 :&&:

-- | Apply a list of types to a type constructor.
--   
--   <pre>
--   &gt;&gt;&gt; :kind! Either :@@: (Int :&amp;&amp;: Bool :&amp;&amp;: LoT0)
--   Either Int Bool :: *
--   </pre>
type family (f :: k) :@@: (tys :: LoT k) :: *
type LoT1 a = a :&&:  'LoT0
type LoT2 a b = a :&&: b :&&: LoT0

-- | Split a type <tt>t</tt> until the constructor <tt>f</tt> is found.
--   
--   <pre>
--   &gt;&gt;&gt; :kind! SplitF (Either Int Bool) Either
--   Int :&amp;&amp;: Bool :&amp;&amp;: LoT0 :: LoT (* -&gt; * -&gt; *)
--   
--   &gt;&gt;&gt; :kind! SplitF (Either Int Bool) (Either Int)
--   Bool :&amp;&amp;: LoT0 :: LoT (* -&gt; *)
--   </pre>
type SplitF (t :: d) (f :: k) = SplitF' t f  'LoT0

-- | Simple natural numbers.
data Nat
Z :: Nat
S :: Nat -> Nat

-- | A type constructor and a list of types that can be applied to it.
data TyEnv
[TyEnv] :: forall k. k -> LoT k -> TyEnv

-- | Split a type <tt>t</tt> until its list of types has length <tt>n</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; :kind! SplitN (Either Int Bool) (S (S Z))
--   TyEnv Either (Int :&amp;&amp;: Bool :&amp;&amp;: LoT0) :: TyEnv
--   
--   &gt;&gt;&gt; :kind! SplitF (Either Int Bool) (S Z)
--   TyEnv (Either Int) (Bool :&amp;&amp;: LoT0) :: TyEnv
--   </pre>
type family SplitN (n :: Nat) t :: TyEnv

module Data.PolyKinded.Atom
data TyVar (d :: *) (k :: TYPE r)
[VZ] :: TyVar (x -> xs) x
[VS] :: TyVar xs k -> TyVar (x -> xs) k
type Var0 =  'Var  'VZ
type Var1 =  'Var ( 'VS  'VZ)
type Var2 =  'Var ( 'VS ( 'VS  'VZ))
type Var3 =  'Var ( 'VS ( 'VS ( 'VS  'VZ)))
type Var4 =  'Var ( 'VS ( 'VS ( 'VS ( 'VS  'VZ))))
type Var5 =  'Var ( 'VS ( 'VS ( 'VS ( 'VS ( 'VS  'VZ)))))
type Var6 =  'Var ( 'VS ( 'VS ( 'VS ( 'VS ( 'VS ( 'VS  'VZ))))))
type Var7 =  'Var ( 'VS ( 'VS ( 'VS ( 'VS ( 'VS ( 'VS ( 'VS  'VZ)))))))
type Var8 =  'Var ( 'VS ( 'VS ( 'VS ( 'VS ( 'VS ( 'VS ( 'VS ( 'VS  'VZ))))))))
type Var9 =  'Var ( 'VS ( 'VS ( 'VS ( 'VS ( 'VS ( 'VS ( 'VS ( 'VS ( 'VS  'VZ)))))))))
data Atom (d :: *) (k :: TYPE r)
[Var] :: TyVar d k -> Atom d k
[Kon] :: k -> Atom d k
[:@:] :: Atom d (k1 -> k2) -> Atom d k1 -> Atom d k2
[:&:] :: Atom d Constraint -> Atom d Constraint -> Atom d Constraint
[ForAll] :: Atom (d1 -> d) * -> Atom d *
[:=>>:] :: Atom d Constraint -> Atom d * -> Atom d *
infixr 5 :=>>:
infixr 5 :&:
type f :$: x =  'Kon f :@: x
type a :~: b =  'Kon (~) :@: a :@: b
type a :~~: b =  'Kon (~~) :@: a :@: b
type family Interpret (t :: Atom d k) (tys :: LoT d) :: k
newtype ForAllI (f :: Atom (d1 -> d) (*)) (tys :: LoT d)
[ForAllI] :: (forall t. Interpret f (t :&&: tys)) -> ForAllI f tys
newtype SuchThatI (c :: Atom d Constraint) (f :: Atom d (*)) (tys :: LoT d)
[SuchThatI] :: (Interpret c tys => Interpret f tys) -> SuchThatI c f tys
type family Satisfies (cs :: [Atom d Constraint]) (tys :: LoT d) :: Constraint
type family ContainsTyVar (v :: TyVar d k) (t :: Atom d p) :: Bool
type family Or (x :: Bool) (y :: Bool) :: Bool


-- | Poly-kinded <a>Functor</a> type class. <a>KFunctor</a> generalizes
--   functors, bifunctors, profunctors, ... by declaring a list of
--   <a>Variance</a>s for a type constructor.
module Data.PolyKinded.Functor

-- | Declares that the type constructor <tt>f</tt> is a generalized functor
--   whose variances for each type argument are given by <tt>v</tt>.
class KFunctor (f :: k) (v :: Variances) (as :: LoT k) (bs :: LoT k) | f -> v

-- | The generalized version of <a>fmap</a>, <tt>bimap</tt>,
--   <tt>dimap</tt>, and so on.
kfmap :: KFunctor f v as bs => Mappings v as bs -> (f :@@: as) -> f :@@: bs

-- | The generalized version of <a>fmap</a>, <tt>bimap</tt>,
--   <tt>dimap</tt>, and so on. This version uses <tt>Split</tt> to obtain
--   better type inference.
kmapo :: forall f v as bs. KFunctor f v as bs => Mappings v as bs -> (f :@@: as) -> f :@@: bs

-- | Possible variances for each argument of a type constructor.
data Variance

-- | The functor is covariant in this position.
Co :: Variance

-- | The functor is contravariant in this position.
Contra :: Variance

-- | This position is not used in any constructor.
Phantom :: Variance
type Variances = [Variance]

-- | If a <a>KFunctor</a> needs to map an <tt>f ... a ...</tt> to an <tt>f
--   ... b ...</tt>, a <tt>Mapping v a b</tt> specifies which function
--   needs to be provided for that position depending on its variance
--   <tt>v</tt>.
type family Mapping (v :: Variance) a b

-- | List of mappings for the list of variances <tt>v</tt>.
data Mappings (v :: Variances) (x :: LoT k) (y :: LoT k)
[M0] :: Mappings '[]  'LoT0  'LoT0
[:^:] :: Mapping v a b -> Mappings vs as bs -> Mappings (v : vs) (a :&&: as) (b :&&: bs)
infixr 5 :^:


-- | Extensions to the <a>GHC.Generics</a> module.
module GHC.Generics.Extra

-- | Constraints: used to represent constraints in a constructor.
--   
--   <pre>
--   data Showable a = Show a =&gt; a -&gt; X a
--   
--   instance Generic (Showable a) where
--     type Rep (Showable a) = (Show a) :=&gt;: (K1 R a)
--   </pre>
data (:=>:) (c :: Constraint) (f :: k -> *) (a :: k)
[SuchThat] :: c => f a -> (c :=>: f) a
