Safe Haskell	None
Language	Haskell2010

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 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 family InterpretVar (t :: TyVar d k) (tys :: LoT d) :: k where ... Source #

Equations

InterpretVar VZ (t :&&: ts) = t
InterpretVar (VS v) (t :&&: ts) = InterpretVar v ts

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

Equations

Interpret (Var v) tys = InterpretVar v tys
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 WrappedI (f :: Atom d *) (tys :: LoT d) Source #

Constructors

WrapI
Fields unwrapI :: Interpret f tys

toWrappedI :: forall f tys t. ForAllI f tys -> WrappedI f (t :&&: tys) Source #

fromWrappedI :: forall f tys. (forall t. WrappedI f (t :&&: tys)) -> ForAllI f tys Source #

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

Constructors

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