sessiontypes-0.1.0: Session types library

Safe HaskellSafe
LanguageHaskell2010

Control.SessionTypes.Types

Contents

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.

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.

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)