kind-apply-0.3.0.0: Utilities to work with lists of types

Data.PolyKinded.Atom

# Documentation

data TyVar (d :: *) (k :: TYPE r) where Source #

Constructors

 VZ :: TyVar (x -> xs) x VS :: TyVar xs k -> TyVar (x -> xs) k

type Var0 = Var VZ Source #

type Var1 = Var (VS VZ) Source #

type Var2 = Var (VS (VS VZ)) Source #

type Var3 = Var (VS (VS (VS VZ))) Source #

type Var4 = Var (VS (VS (VS (VS VZ)))) Source #

type Var5 = Var (VS (VS (VS (VS (VS VZ))))) Source #

type Var6 = Var (VS (VS (VS (VS (VS (VS VZ)))))) Source #

type Var7 = Var (VS (VS (VS (VS (VS (VS (VS VZ))))))) Source #

type Var8 = Var (VS (VS (VS (VS (VS (VS (VS (VS VZ)))))))) Source #

type Var9 = Var (VS (VS (VS (VS (VS (VS (VS (VS (VS VZ))))))))) Source #

data Atom (d :: *) (k :: TYPE r) where Source #

Constructors

 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 infixr 5 ForAll :: Atom (d1 -> d) * -> Atom d * (:=>>:) :: Atom d Constraint -> Atom d * -> Atom d * infixr 5

type (:\$:) f x = Kon f :@: x Source #

type (:~:) a b = (Kon (~) :@: a) :@: b Source #

type (:~~:) a b = (Kon (~~) :@: a) :@: b Source #

type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where ... Source #

Equations

 Interpret (Var VZ) (t :&&: ts) = t Interpret (Var (VS v)) (t :&&: ts) = Interpret (Var v) ts Interpret (Kon t) tys = t Interpret (f :@: x) tys = Interpret f tys (Interpret x tys) Interpret (c :&: d) tys = (Interpret c tys, Interpret d tys) Interpret (ForAll f) tys = ForAllI f tys Interpret (c :=>>: f) tys = SuchThatI c f tys

newtype ForAllI (f :: Atom (d1 -> d) *) (tys :: LoT d) where Source #

Constructors

 ForAllI :: (forall t. Interpret f (t :&&: tys)) -> ForAllI f tys

newtype SuchThatI (c :: Atom d Constraint) (f :: Atom d *) (tys :: LoT d) where Source #

Constructors

 SuchThatI :: (Interpret c tys => Interpret f tys) -> SuchThatI c f tys

type family Satisfies (cs :: [Atom d Constraint]) (tys :: LoT d) :: Constraint where ... Source #

Equations

 Satisfies '[] tys = () Satisfies (c ': cs) tys = (Interpret c tys, Satisfies cs tys)

type family ContainsTyVar (v :: TyVar d k) (t :: Atom d p) :: Bool where ... Source #

Equations

 ContainsTyVar v (Var v) = True ContainsTyVar v (Var w) = False ContainsTyVar v (Kon t) = False ContainsTyVar v (f :@: x) = Or (ContainsTyVar v f) (ContainsTyVar v x) ContainsTyVar v (x :&: y) = Or (ContainsTyVar v x) (ContainsTyVar v y) ContainsTyVar v (c :=>>: f) = Or (ContainsTyVar v c) (ContainsTyVar v f) ContainsTyVar v (ForAll f) = ContainsTyVar (VS v) f

type family Or (x :: Bool) (y :: Bool) :: Bool where ... Source #

Equations

 Or True thing = True Or thing True = True Or False False = False