Control.SessionTypes

STTerm

data STTerm

inferIdentity

MonadSession

Primitives

class MonadSession m

Combinators

empty

empty0

selN

selN1

selN2

selN3

selN4

class Select xs s

(<&)

(<&>)

offer

recurseFix

recurse0

weaken0

var0

eps0

Types

Session Types

data ST a

data Cap a

type family GetST s where ...

type family GetCtx s where ...

Duality

type family Dual s = r | r -> s where ...

type family DualST (a :: ST c) = (b :: ST c) | b -> a where ...

type family MapDual xs = ys | ys -> xs where ...

Removing

type family RemoveSend s where ...

type family RemoveSendST s where ...

type family MapRemoveSend ctx where ...

type family RemoveRecv s where ...

type family RemoveRecvST s where ...

type family MapRemoveRecv ctx where ...

Applying Constraints

type family HasConstraint (c :: Type -> Constraint) s :: Constraint where ...

type family HasConstraintST (c :: Type -> Constraint) s :: Constraint where ...

type family MapHasConstraint (c :: Type -> Constraint) ss :: Constraint where ...

type family HasConstraints (cs :: [Type -> Constraint]) s :: Constraint where ...

Boolean functions

type family IfThenElse (b :: Bool) (l :: k) (r :: k) :: k where ...

type family Not b :: Bool where ...

type family Or b1 b2 :: Bool where ...

Product type

data Prod t

type family Left p where ...

type family Right p where ...

Other

data Nat

data Ref s xs

type family TypeEqList xs s where ...

type family Append xs ys where ...