| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Control.SessionTypes.Normalize
Description
This module provides a type class for normalizing session typed programs.
With normalizing we mean that we apply rewrites to a session typed program until we can no longer do so and that do not change the semantics of the program.
The motivation for this module is that for two session typed programs to run a session they must be dual. Sometimes, one of these programs might not have a session type that is dual to the session type of the other program,
but we can rewrite the program and therefore also the session type such that it is. It is of course important that we do not alter the semantics of the program when rewriting it. For that reason, any rewrite that we may apply must be isomorphic.
A rewrite is isomorphic if we have two programs p and p', we can do a rewrite from p to p' and from p' to p.
For now two types of rewrites are applied: Elimination of recursive types and flattening of branches.
Documentation
class Normalize s s'' | s -> s'' where Source #
Type class for rewriting an STTerm to its normal form
The type class has a single instance that is constrained with two type classes. One for each type of rewrite.
Minimal complete definition
class Flatten s s' | s -> s' where Source #
Type class for flattening branches
The function flatten takes and traverses a STTerm.
If it finds a branching session type that has a branch
starting with another branching of the same type, then it will extract the branches of the inner branching
and inserts these into the outer branching. This is similar to flattening a list of lists to a larger list.
For example:
Sel '[a,b, Sel '[c,d], e]
becomes
Sel '[a,b,c,d,e]
This only works if the inner branching has the same type as the outer branch (Sel in Sel or Off in Off).
Also, for now this rewrite only works if one of the branching of the outer branch starts with a new branching.
For example:
Sel '[a,b, Int :!> Sel '[c,d],e]
does not become
Sel '[a,b,Int :!> c, Int :!> d, e]
This is something that will be added in the future.
Minimal complete definition
class ElimRec s s' | s -> s' where Source #
Type class for eliminating unused recursive types.
The function elimRec traverses a given STTerm. While doing so, it will attempt to remove constructors annotated with R or Wk from the program
if in doing so does not change the behavior of the program.
For example, in the following session type we may remove the inner R and the Wk.
R (R (Wk V))
We have that the outer R matches the recursion variable because of the use of Wk.
That means the inner R does not match any recursion variable (the R is unused) and therefore may it and its corresponding constructor be removed from the STTerm program.
We also remove the Wk, because the session type pushed into the context by the inner R has also been removed.
The generated session type is
R V
Minimal complete definition