Control.Distributed.Session.Normalize

This module provides three functions 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 as 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 its session type. 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.

An additional benefit of normalizing is that it may lead to further optimizations.

In Control.Distributed.Session.Eval we send an integer for every Sel session type that we encounter. By flattening branching we reduce the number of Sel constructors and therefore also the number of times one needs to communicate an integer.

Documentation

normalize :: Normalize s s' => Session s (Cap '[] Eps) a -> Session s' (Cap '[] Eps) a

Applies two types of rewrites to a Session.

• Elimination of unused recursion
• Rewrites non-right nested branchings to right nested branchings

elimRec :: ElimRec s s' => Session s (Cap '[] Eps) a -> Session s' (Cap '[] Eps) a

Function for eliminating unused recursive types.

The function elimRec takes a Session and traverses the underlying STTerm. While doing so, it will attempt to remove STTerm 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 session.

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

flatten :: Flatten s s' => Session s (Cap '[] Eps) a -> Session s' (Cap '[] Eps) a

Flattening of branching

The function flatten takes a Session and traverses the underlying 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]

Although, this is something that will be added in the future.