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

Safe HaskellNone
LanguageHaskell2010

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 #

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

Equations

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