Safe Haskell	Safe
Language	Haskell2010

Control.SessionTypes.Types

Contents

Session Types
Duality
Removing
Applying Constraints
Boolean functions
Product type
Other

Description

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.

Synopsis

Session Types

data ST a Source #

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 Source #

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) Source #
Methods (>>=) :: m s t a -> (a -> m t k b) -> m s k b Source # (>>) :: m s t a -> m t k b -> m s k b Source # return :: a -> m i i a Source # fail :: String -> m i i a Source #
IxApplicative (Cap *) (IxC m) Source #
Methods pure :: a -> f i i a Source # (<*>) :: f s r (a -> b) -> f r k a -> f s k b Source #
IxFunctor (Cap *) (IxC m) Source #
Methods fmap :: (a -> b) -> f j k a -> f j k b Source #
Monad m => IxMonadT (Cap a) (STTerm a) m Source #
Methods lift :: m a -> m m s s a Source #
MonadIO m => IxMonadIO (Cap a) (STTerm a m) Source #
Methods liftIO :: IO a -> m s s a Source #
Monad m => IxMonad (Cap a) (STTerm a m) Source #
Methods (>>=) :: m s t a -> (a -> m t k b) -> m s k b Source # (>>) :: m s t a -> m t k b -> m s k b Source # return :: a -> m i i a Source # fail :: String -> m i i a Source #
Monad m => IxApplicative (Cap a) (STTerm a m) Source #
Methods pure :: a -> f i i a Source # (<*>) :: f s r (a -> b) -> f r k a -> f s k b Source #
IxFunctor (Cap a) (STTerm a m) Source #
Methods fmap :: (a -> b) -> f j k a -> f j k b Source #

type family GetST s where ... Source #

Retrieves the session type from the capability

Equations

GetST (Cap ctx s) = s

type family GetCtx s where ... Source #

Retrieves the context from the capability

Equations

GetCtx (Cap ctx s) = ctx

Duality

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

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

Promoted ifThenElse

Equations

IfThenElse True l r = l
IfThenElse False l r = r

type family Not b :: Bool where ... Source #

Promoted not

Equations

Not True = False
Not False = True

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

Promoted ||

Equations

Or True b = True
Or b True = True
Or b1 b2 = False

Product type

data Prod t Source #

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 ... Source #

Type family for returning the first argument of a product.

Equations

Left (l :*: r) = l

type family Right p where ... Source #

Type family for returning the second argument of a product.

Equations

Right (l :*: r) = r

Other

data Nat Source #

Data type defining natural numbers

Constructors

Z
S Nat

Instances

Eq Nat Source #
Methods (==) :: Nat -> Nat -> Bool # (/=) :: Nat -> Nat -> Bool #
Ord Nat Source #
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 Source #
Methods showsPrec :: Int -> Nat -> ShowS # show :: Nat -> String # showList :: [Nat] -> ShowS #

data Ref s xs where Source #

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 ... Source #

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 ... Source #

Promoted ++

Equations

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