| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Control.SessionTypes.STTerm
Description
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.
- data STTerm :: (Type -> Type) -> Cap a -> Cap a -> Type -> Type where
- Send :: a -> STTerm m (Cap ctx r) r' b -> STTerm m (Cap ctx (a :!> r)) r' b
- Recv :: (a -> STTerm m (Cap ctx r) r' b) -> STTerm m (Cap ctx (a :?> r)) r' b
- Sel1 :: STTerm m (Cap ctx s) r a -> STTerm m (Cap ctx (Sel (s ': xs))) r a
- Sel2 :: STTerm m (Cap ctx (Sel (t ': xs))) r a -> STTerm m (Cap ctx (Sel (s ': (t ': xs)))) r a
- OffZ :: STTerm m (Cap ctx s) r a -> STTerm m (Cap ctx (Off '[s])) r a
- 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
- Rec :: STTerm m (Cap (s ': ctx) s) r a -> STTerm m (Cap ctx (R s)) r a
- Weaken :: STTerm m (Cap ctx t) r a -> STTerm m (Cap (s ': ctx) (Wk t)) r a
- Var :: STTerm m (Cap (s ': ctx) s) t a -> STTerm m (Cap (s ': ctx) V) t a
- Ret :: (a :: Type) -> STTerm m s s a
- Lift :: m (STTerm m s r a) -> STTerm m s r a
- inferIdentity :: STTerm Identity s r a -> STTerm Identity s r a
Documentation
data STTerm :: (Type -> Type) -> Cap a -> Cap a -> Type -> Type where Source #
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:
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 |
| 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 |
| 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 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 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 |
| Ret :: (a :: Type) -> STTerm m s s a | Constructor that makes |
| Lift :: m (STTerm m s r a) -> STTerm m s r a | Constructor that makes |
Instances
| Monad m => IxMonadT (Cap a) (STTerm a) m Source # | |
| MonadIO m => IxMonadIO (Cap a) (STTerm a m) Source # | |
| Monad m => IxMonad (Cap a) (STTerm a m) Source # | |
| Monad m => IxApplicative (Cap a) (STTerm a m) Source # | |
| Monad m => IxFunctor (Cap a) (STTerm a m) Source # | |
| Monad m => MonadSession (STTerm * m) Source # | |
| Monad (STTerm a m s s) Source # | |
| Functor (STTerm a m s s) Source # | |
| Applicative (STTerm a m s s) Source # | |