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

For example:

```
!Int ; ?Bool
!Int ; ?Bool
```

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
```

**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)`

.

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)
```

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
```

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