Control.SessionTypes.Types

This module provides a collection of types and type families.

Specifically it defines the session type data type, capability data type and type families that compute using session types or capabilities as arguments.

Session Types

data ST a

The session type data type

Each constructor denotes a specific session type. Using the DataKinds pragma the constructors are promoted to types and ST is promoted to a kind.

Constructors

(:?>) a (ST a) infixr 6

Send a value

(:!>) a (ST a) infixr 6

Recv a value

Sel [ST a]

Selection of branches

Off [ST a]

Offering of branches

R (ST a)

Delimit the scope of recursion

Wk (ST a)

Weaken the scope of recursion

V

Recursion variable

Eps

End of the session

data Cap a

A capability that stores a context/scope that is a list of session types and a session type

Constructors

Cap [ST a] (ST a)

Instances

IxMonad (Cap *) (IxC m)

Methods

(>>=) :: m s t a -> (a -> m t k b) -> m s k b

(>>) :: m s t a -> m t k b -> m s k b

return :: a -> m i i a

fail :: String -> m i i a

IxApplicative (Cap *) (IxC m)

Methods

pure :: a -> f i i a

(<*>) :: f s r (a -> b) -> f r k a -> f s k b

IxFunctor (Cap *) (IxC m)

Methods

fmap :: (a -> b) -> f j k a -> f j k b

Monad m => IxMonadT (Cap a) (STTerm a) m

Methods

lift :: m a -> m m s s a

MonadIO m => IxMonadIO (Cap a) (STTerm a m)

Methods

liftIO :: IO a -> m s s a

Monad m => IxMonad (Cap a) (STTerm a m)

Methods

(>>=) :: m s t a -> (a -> m t k b) -> m s k b

(>>) :: m s t a -> m t k b -> m s k b

return :: a -> m i i a

fail :: String -> m i i a

Monad m => IxApplicative (Cap a) (STTerm a m)

Methods

pure :: a -> f i i a

(<*>) :: f s r (a -> b) -> f r k a -> f s k b

IxFunctor (Cap a) (STTerm a m)

Methods

fmap :: (a -> b) -> f j k a -> f j k b

type family GetST s where ...

Retrieves the session type from the capability

Equations

GetST (Cap ctx s) = s

type family GetCtx s where ...

Retrieves the context from the capability

Equations

GetCtx (Cap ctx s) = ctx

Duality

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

Type family for calculating the dual of a session type. It may be applied to a capability.

We made Dual injective to support calculating the dual of a selection that contains an ambiguous branch. Of course that does require that the dual of that ambiguous branch must be known.

Equations

Dual (Cap ctx s) = Cap (MapDual ctx) (DualST s)

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

Type family for calculating the dual of a session type. It may be applied to the actual session type.

Equations

DualST (s :!> r) = s :?> DualST r

DualST (s :?> r) = s :!> DualST r

DualST (Sel xs) = Off (MapDual xs)

DualST (Off xs) = Sel (MapDual xs)

DualST (R s) = R (DualST s)

DualST (Wk s) = Wk (DualST s)

DualST V = V

DualST Eps = Eps

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

Type family for calculating the dual of a list of session types.

Equations

MapDual '[] = '[]

MapDual (s ': xs) = DualST s ': MapDual xs

Removing

type family RemoveSend s where ...

Type family for removing the send session type from the given session type. It may be applied to a capability.

Equations

RemoveSend (Cap ctx s) = Cap (MapRemoveSend ctx) (RemoveSendST s)

type family RemoveSendST s where ...

Type family for removing the send session type from the given session type. It may be applied to a session type.

Equations

RemoveSendST (a :!> r) = RemoveSendST r

RemoveSendST (a :?> r) = a :?> RemoveSendST r

RemoveSendST (Sel xs) = Sel (MapRemoveSend xs)

RemoveSendST (Off xs) = Off (MapRemoveSend xs)

RemoveSendST (R s) = R (RemoveSendST s)

RemoveSendST (Wk s) = Wk (RemoveSendST s)

RemoveSendST s = s

type family MapRemoveSend ctx where ...

Type family for removing the send session type from a list of session types.

Equations

MapRemoveSend '[] = '[]

MapRemoveSend (s ': ctx) = RemoveSendST s ': MapRemoveSend ctx

type family RemoveRecv s where ...

Type family for removing the receive session type from the given session type. It may be applied to a capability.

Equations

RemoveRecv (Cap ctx s) = Cap (MapRemoveRecv ctx) (RemoveRecvST s)

type family RemoveRecvST s where ...

Type family for removing the receive session type from a list of session types.

Equations

RemoveRecvST (a :!> r) = a :!> RemoveRecvST r

RemoveRecvST (a :?> r) = RemoveRecvST r

RemoveRecvST (Sel xs) = Sel (MapRemoveRecv xs)

RemoveRecvST (Off xs) = Off (MapRemoveRecv xs)

RemoveRecvST (R s) = R (RemoveRecvST s)

RemoveRecvST (Wk s) = Wk (RemoveRecvST s)

RemoveRecvST s = s

type family MapRemoveRecv ctx where ...

Type family for removing the receive session type from the given session type. It may be applied to a session type.

Equations

MapRemoveRecv '[] = '[]

MapRemoveRecv (s ': ctx) = RemoveRecvST s ': MapRemoveRecv ctx

Applying Constraints

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

Type family for applying a constraint to types of kind Type in a session type. It may be applied to a capability.

Equations

HasConstraint c (Cap ctx s) = (HasConstraintST c s, MapHasConstraint c ctx)

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

Type family for applying a constraint to types of kind Type in a list of session types.

Equations

HasConstraintST c (a :!> r) = (c a, HasConstraintST c r)

HasConstraintST c (a :?> r) = (c a, HasConstraintST c r)

HasConstraintST c (Sel '[]) = ()

HasConstraintST c (Sel (s ': xs)) = (HasConstraintST c s, HasConstraintST c (Sel xs))

HasConstraintST c (Off '[]) = ()

HasConstraintST c (Off (s ': xs)) = (HasConstraintST c s, HasConstraintST c (Off xs))

HasConstraintST c (R s) = HasConstraintST c s

HasConstraintST c (Wk s) = HasConstraintST c s

HasConstraintST c V = ()

HasConstraintST c s = ()

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

Type family for applying a constraint to types of kind Type in a session type. It may be applied to a session type.

Equations

MapHasConstraint c '[] = ()

MapHasConstraint c (s ': ss) = (HasConstraintST c s, MapHasConstraint c ss)

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

Type family for applying zero or more constraints to types of kind Type in a list of session types. It may be applied to a capability.

Equations

HasConstraints '[] s = ()

HasConstraints (c ': cs) s = (HasConstraint c s, HasConstraints cs s)

Boolean functions

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

Promoted ifThenElse

Equations

IfThenElse True l r = l

IfThenElse False l r = r

type family Not b :: Bool where ...

Promoted not

Equations

Not True = False

Not False = True

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

Promoted ||

Equations

Or True b = True

Or b True = True

Or b1 b2 = False

Product type

data Prod t

Data type that takes a kind as an argument. Its sole constructor takes two capabilities parameterized by the kind argument.

This data type is useful if it is necessary for an indexed monad to be indexed by four parameters.

Constructors

(:*:) (Cap t) (Cap t)

type family Left p where ...

Type family for returning the first argument of a product.

Equations

Left (l :*: r) = l

type family Right p where ...

Type family for returning the second argument of a product.

Equations

Right (l :*: r) = r

Other

data Nat

Data type defining natural numbers

Constructors

Z

S Nat

Instances

Eq Nat

Methods

(==) :: Nat -> Nat -> Bool

(/=) :: Nat -> Nat -> Bool

Ord Nat

Methods

compare :: Nat -> Nat -> Ordering

(<) :: Nat -> Nat -> Bool

(<=) :: Nat -> Nat -> Bool

(>) :: Nat -> Nat -> Bool

(>=) :: Nat -> Nat -> Bool

max :: Nat -> Nat -> Nat

min :: Nat -> Nat -> Nat

Show Nat

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

data Ref s xs where

Data type that can give us proof of membership of an element in a list of elements.

Constructors

RefZ :: Ref s (s ': xs)

RefS :: Ref s (k ': xs) -> Ref s (t ': (k ': xs))

type family TypeEqList xs s where ...

Type family for computing which types in a list of types are equal to a given type.

Equations

TypeEqList '[s] s = '[True]

TypeEqList '[r] s = '[False]

TypeEqList (s ': xs) s = True ': TypeEqList xs s

TypeEqList (r ': xs) s = False ': TypeEqList xs s

type family Append xs ys where ...

Promoted ++

Equations

Append '[] ys = ys

Append (x ': xs) ys = x ': (xs `Append` ys)