Equivalence of Context-free Session Types

Usage

Type two types (see syntax below) separated by a new line character.

For example:

!Int ; ?Bool
!Int ; ?Bool

The Syntax of Types

Session Types

The session types that describe message exchanges are the following:

• Message sending: !B
• Message reception: ?B

where B is one of the basic types: Int, Bool, Char, or (). For example, a type that describes the output of an integer is !Int.

• Sequential composition: Types are composed sequentially through operator ;. If T1 and T2 are two types, then T1 ; T2 is a type. For example, to send an integer and then receive a boolean value we compose both operations with sequential composition, to obtain: !Int;?Bool.

• Skip: Type Skip represents ... well, a type that can be skipped. The following two types are equivalent

Skip ; !Int
!Int

and so are these

!Int ; Skip
!Int

But type Skip by itself denotes no interaction.

• Internal choice: A choice among multiple alternatives, as seen from the side that choses. An internal choice is of the form +{l1:T1, ..., ln:Tn}, where T1, ..., Tn are session types and l1, ..., ln are labels denoting the different choices. Labels must be pairwise distinct. For example, a choice between sending an integer and receiving a boolean can be described as follows:

  +{IntChoice: !Int, BoolChoice: ?Bool}

The order of the labels is unimportant. These two types are equivalent:

+{IntChoice: !Int, BoolChoice: ?Bool}
+{BoolChoice: ?Bool, IntChoice: !Int}

• External choice: A choice among multiple alternatives, as seen from the side that must provide all options. An external choice is of the form &{l1:T1, ..., ln:Tn}, similar to the internal choice but with a view & in place of +. As an example, the type that offers two alternatives, receiving an integer or sending a boolean can be written as follows

  &{IntChoice: ?Int, BoolChoice: !Bool}

• Recursive types: Recursive types allow describing unbounded behaviour. Towards this end two new types are introduced: rec x. T and x. A type that sending integer values for ever can be written as rec x. !Int ; x. A recursive type is equivalent to its unfolding:

rec x. !Int ; x
!Int ; rec x. !Int ; x

The recursion variable need not appear in tail position, and it may appear more than once. This is the essence of context-free session types.

rec x. !Int ; x ; !Int
rec x. !Int ; x ; x ; x ; x

The name of the recursion variable is unimportant. The following two types are equivalent:

rec x. !Int ; x
rec y. !Int ; y

Functional Types

• Basic Types: These are the set of basic types as introduced before: Int, Bool, Char, and ()

• Linear Function Type: A linear function type must be used exactly once. A linear function that expects a type T1 and returns a type T2 is written T1 -o T2.

• Unrestricted Function Type: These are the functions can be used an unbound number of times, including zero and one. An unrestricted function that expects a type T1 and returns a type T2 is written T1 -> T2. Linear functions are not equivalent to their unrestricted counterparts, even if the input/output behaviour matches:

!Int -o ?Char 
!Int -> ?Char 

• Pairs: A pair composed of types T1 and T2 is written (T1, T2).

Polymorphism

Polymorphic types (or type schemes) rely on polymorphic variables. Type variables can be introduced by a rec type or by a forall. In the former case we call it a recursion variable, in the latter, a polymorphic variable. In any case, variables must be explicitly introduced in types: !Int ; x is not a type. For example, the type of the identity function is written as follows:

forall a => a -> a

Here is a session type that repeatedly performs some action a. Type variable a must denote a session type (and not a functional type), which is the default annotation for polymorphic variables.

forall a => rec y. a ; y
forall a => rec y. a ; y ; a

And here is the type of a function that receives an integer value on some channel and returns the integer and the continuation:

forall a => ?Int ; a -o (Int, a)

Type Formation

Not all syntax generated by the grammar (informally) introduced above makes sense. Here are a few restrictions:

• All variables must be introduced by a rec or a forall,
• Types underneath a rec must not be terminated: a terminated type is composed exclusively of Skip, ;, and rec, and
• There can be no functional types within session types.

Below are a few ill-formed types:

x
forall x => rec y. !Bool ; z
rec x. x
rec x. Skip
rec x. Skip ; Skip ; Skip
rec x. rec y. rec z. x
rec x. rec y. rec z. (Skip ; x; Skip ; !Int)
Char ; !Int
(!Int -> ?Bool) ; Skip

Type variables introduced with forall may be annotated with a pre-kind S if T, followed by a multiplicity U or S. Prekind T is for functional types; pre-kind S is for session types. Multiplicity U is for those resources that may used zero or more times (unrestricted); multiplicity L is of resources that must be used exactly once (linear). The absence of annotation for a given polymorphic variable is taken as SL.

Below are a few more ill-formed types

forall a: TU => a; !Int
forall b: TL => ?Bool; b

These two types are both well formed, but have different meanings: Bool -> !Int is a valid instance of the former but not of the latter.

forall a: TL => a -> !Int
forall b: SL => b -> !Int

Some Equivalence Laws

Context-free session types are associative (sequential composition is right-associative):

!Int ; (!Bool ; !Char)
(!Int ; !Bool) ; !Char 

Skip is left-neutral:

Skip ; !Int
!Int 

and right-neutral:

!Int ; Skip
!Int 

Choice (either internal or external) right-distributes over sequential composition:

+{Read: ?Char, Write: !Int} ; !Bool 
+{Read: ?Char ; ! Bool, Write: !Int ; !Bool}

Unfolding recursive types preserves equivalence:

rec x. !Char ; x 
!Char ; rec x. !Char ; x 

And there are equivalent types that cannot be transformed into one another by simple unfolding (this is not particular to context-free session types):

rec x. !Char ; ?Int ; x 
!Char ; rec y. ?Int ; !Char ; y

rec types whose var does not occur free in the body of recursion can be elided:

rec x. !Char
!Char

Two rec types in a row can be joined together provided we rename the free occurrences of the variable that "disappears":

rec x. rec y. !Char ; x ; y 
rec x. !Char ; x ; x

In this case, the last variable is "unreachable" and can be omitted:

rec x. !Char ; x ; x
rec x. !Char ; x 

In general, a type T1 is equivalent to T1;T2 when T1 is unnormed. We say that a type is normed when it contains a path that leads to Skip. Types rec x. !Char ; x ; x is unnormed. Choice can transform an unnormed type into a normed one, for example: rec x. {Out: !Char ; x ; x, Done: Skip} is normed. In this case we cannot remove the "second" x:

rec x. +{Out: !Char ; x ; x, Done: Skip} 
rec x. +{Out: !Char ; x, Done: Skip} 

For details on context-free session types, see P. Thiemann, V. T. Vasconcelos. Context-free session types. ACM SIGPLAN Notices. Vol. 51. No. 9. ACM, 2016