Control.SessionTypes.STTerm

This module defines a GADT STTerm that is the very core of this library

Session typed programs are constructed by composing the constructors of STTerm.

Each constructor is annotated with a specific session type (except for Ret and Lift).

By passing a constructor to another constructor as an argument their session types are joined to form a larger session type.

We do not recommend explicitly composing the STTerm constructors. Instead make use of the functions defined in the Control.SessionTypes.MonadSession module.

Of course a STTerm program in itself is not very useful as it is devoid of any semantics. However, an interpreter function can give meaning to a STTerm program.

We define a couple in this library: Control.SessionTypes.Debug, Control.SessionTypes.Interactive, Control.SessionTypes.Normalize and Control.SessionTypes.Visualize.

Documentation

data STTerm :: (Type -> Type) -> Cap a -> Cap a -> Type -> Type where

The STTerm GADT

Although we say that a STTerm is annotated with a session type, it is actually annotated with a capability (Cap).

The capability contains a context that is necessary for recursion and the session type.

The constructors can be split in four different categories:

• Communication: Send and Recv for basic communication
• Branching: Sel1, Sel2, OffZ and OffS
• Recursion: Rec, Weaken and Var
• Unsession typed: Ret and Lift

Constructors

Send :: a -> STTerm m (Cap ctx r) r' b -> STTerm m (Cap ctx (a :!> r)) r' b

The constructor for sending messages. It is annotated with the send session type (:!>).

It takes as an argument, the message to send, of type equal to the first argument of :!> and the continuing STTerm that is session typed with the second argument of :!>.

Recv :: (a -> STTerm m (Cap ctx r) r' b) -> STTerm m (Cap ctx (a :?> r)) r' b

The constructor for receiving messages. It is annotated with the receive session type (:?>)

It takes a continuation that promises to deliver a value that may be used in the rest of the program.

Sel1 :: STTerm m (Cap ctx s) r a -> STTerm m (Cap ctx (Sel (s ': xs))) r a

Selects the first branch in a selection session type.

By selecting a branch, that selected session type must then be implemented.

Sel2 :: STTerm m (Cap ctx (Sel (t ': xs))) r a -> STTerm m (Cap ctx (Sel (s ': (t ': xs)))) r a

Skips a branch in a selection session type.

If the first branch in the selection session type is not the one we want to implement then we may use Sel2 to skip this.

OffZ :: STTerm m (Cap ctx s) r a -> STTerm m (Cap ctx (Off '[s])) r a

Dually to selection there is also offering branches.

Unlike selection, where we may only implement one branch, an offering asks you to implement all branches. Which is chosen depends on how an interpreter synchronizes selection with offering.

This constructor denotes the very last branch that may be offered.

OffS :: STTerm m (Cap ctx s) r a -> STTerm m (Cap ctx (Off (t ': xs))) r a -> STTerm m (Cap ctx (Off (s ': (t ': xs)))) r a

offers a branch and promises at least one more branch to be offered.

Rec :: STTerm m (Cap (s ': ctx) s) r a -> STTerm m (Cap ctx (R s)) r a

Constructor for delimiting the scope of recursion

The recursion constructors also modify or at least make use of the context in the capability.

The Rec constructor inserts the session type argument to R into the context of the capability of its STTerm argument.

This is necessary such that we remember the session type of the body of code that we may want to recurse over and thus avoiding infinite type occurrence errors.

Weaken :: STTerm m (Cap ctx t) r a -> STTerm m (Cap (s ': ctx) (Wk t)) r a

Constructor for weakening (expanding) the scope of recusion

This constructor does the opposite of R by popping a session type from the context.

Use this constructor to essentially exit a recursion

Var :: STTerm m (Cap (s ': ctx) s) t a -> STTerm m (Cap (s ': ctx) V) t a

Constructor that denotes the recursion variable

It assumes the context to be non-empty and uses the session type at the top of the context to determine what should be implemented after Var.

Ret :: (a :: Type) -> STTerm m s s a

Constructor that makes STTerm a (indexed) monad

Lift :: m (STTerm m s r a) -> STTerm m s r a

Constructor that makes STTerm a (indexed) monad transformer

Instances

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

Monad m => MonadSession (STTerm * m)

Methods

send :: a -> STTerm * m (Cap * ctx ((* :!> a) r)) (Cap * ctx r) ()

recv :: STTerm * m (Cap * ctx ((* :?> a) r)) (Cap * ctx r) a

sel1 :: STTerm * m (Cap * ctx (Sel * ((ST * ': s) xs))) (Cap * ctx s) ()

sel2 :: STTerm * m (Cap * ctx (Sel * ((ST * ': s) ((ST * ': t) xs)))) (Cap * ctx (Sel * ((ST * ': t) xs))) ()

offZ :: STTerm * m (Cap * ctx s) r a -> STTerm * m (Cap * ctx (Off * ((ST * ': s) [ST *]))) r a

offS :: STTerm * m (Cap * ctx s) r a -> STTerm * m (Cap * ctx (Off * ((ST * ': t) xs))) r a -> STTerm * m (Cap * ctx (Off * ((ST * ': s) ((ST * ': t) xs)))) r a

recurse :: STTerm * m (Cap * ((ST * ': s) ctx) s) r a -> STTerm * m (Cap * ctx (R * s)) r a

weaken :: STTerm * m (Cap * ctx s) r a -> STTerm * m (Cap * ((ST * ': t) ctx) (Wk * s)) r a

var :: STTerm * m (Cap * ((ST * ': s) ctx) s) r a -> STTerm * m (Cap * ((ST * ': s) ctx) (V *)) r a

eps :: a -> STTerm * m (Cap * ctx (Eps *)) (Cap * ctx (Eps *)) a

Monad (STTerm a m s s)

Methods

(>>=) :: STTerm a m s s a -> (a -> STTerm a m s s b) -> STTerm a m s s b

(>>) :: STTerm a m s s a -> STTerm a m s s b -> STTerm a m s s b

return :: a -> STTerm a m s s a

fail :: String -> STTerm a m s s a

Functor (STTerm a m s s)

Methods

fmap :: (a -> b) -> STTerm a m s s a -> STTerm a m s s b

(<$) :: a -> STTerm a m s s b -> STTerm a m s s a

Applicative (STTerm a m s s)

Methods

pure :: a -> STTerm a m s s a

(<*>) :: STTerm a m s s (a -> b) -> STTerm a m s s a -> STTerm a m s s b

(*>) :: STTerm a m s s a -> STTerm a m s s b -> STTerm a m s s b

(<*) :: STTerm a m s s a -> STTerm a m s s b -> STTerm a m s s a

inferIdentity :: STTerm Identity s r a -> STTerm Identity s r a

This function can be used if we do not use lift in a program but we must still disambiguate m.