A.3 Types

A.3.1 Simple types

Types are associated at a fundamental level with the set of elements that the type contains. Type expressions can occur only as part of the definition of channels or other types, but the name of a type can be used anywhere that a set is required.

For example, the type of integer values is Int and the type of boolean values is Bool, so

{0..3} <= Int
{true, false} == Bool

Proc is the type of Processes, so processes can be put into datatypes:

datatype D = P.Proc | I.Int

In type expressions the tuple syntax denotes a product type and the dot operation denotes a composite type so that

({0,1},{2,3}) denotes {(0,2),(0,3),(1,2),(1,3)}
{0,1}.{2,3} denotes {0.2, 0.3, 1.2, 1.3}

The Set and Seq functions which return the powerset and sequence-space of their arguments are also useful in type expressions.

A.3.2 Named types

Nametype definitions associate a name with a type expression, meaning that ‘.’ and ‘( , , )’ operate on it as type constructors rather than value expressions. The type name may not take parameters.

For example,

nametype Values = {0..199}
nametype Ranges = Values . Values

has the same effect as

Values = {0..199}
Ranges = { x.y | x<-Values, y<-Values }

Note that outside of the ‘top-level’ of a nametype (or datatype, or subtype) definition, the expression ‘Values . Values’ has the entirely different meaning of two copies of the set Values joined by the infix dot. Similarly the expression ‘(Values,Values)’ means the cartesian product of Values for the construction of a type, but a pair of two sets in all other contexts.

A.3.3 Datatypes

Syntax

datatype T = A.{0..3} | B.Set({0,1}) | C	definition of type
A.0, B.{0}, B.{0,1}, C	four uses of type

Remarks

Datatypes may not be parameterised (T may not have arguments).

The datatype corresponds to the variant-record construct of languages like Pascal. At the simplest level it can be used to define a number of atomic constants

datatype SimpleColour = Red | Green | Blue

but values can also be associated with the tags

Gun = {0..15}
datatype ComplexColour = RGB.Gun.Gun.Gun | Grey.Gun | Black | White

Values are combined with ‘.’ and labelled using the appropriate tag, so that we could write

make_colour((r.g.b)@@x) =
  if r!=g or g!=b then RGB.x else
  if r==0 then Black else
  if r==15 then White else Grey.r

to encode a colour as briefly as possible.

Note that while it is possible to write

datatype SlowComplexColour = RGB.{r.g.b | r<-Gun, g<-Gun, b<-Gun} | ...

this is less efficient and the resulting type must still be rectangular, i.e., expressible as a simple product type. Hence it is not legal to write

datatype BrokenComplexColour = -- NOT RECTANGULAR
  RGB.{r.g.b | r<-Gun, g<-Gun, b<-Gun, r+g+b < 30 } | ...

A.3.4 Subtypes

Syntax

subtype U = A.{0,2} | C

definition of subtype

Remarks

A subtype definition associates a name (U) with a subset of an existing type. The tags (A and C in the example) are assumed to have been defined as part of a datatype definition, with bodies which are supersets of those given in the subtype definition.

As with nametype, the same effect can be expressed by defining the type in terms of set comprehensions, but this can be less clear and less efficient.

A.3.5 Channels

Syntax

channel flip, flop	simple channels
channel c, d : {0..3}.LEVEL	channels with more complex protocol
Events	the type of all defined events

Remarks

Channels are tags which form the basis for events. A channel becomes an event when enough values have been supplied to complete it (for example flop above is an event). In the same way that, given

datatype T = A.{0..3} | ...

we know that A.1 is a value of type T, given

channel c : {0..3}

we know that c.1 is a value of type Event. Indeed, the channel definitions in a script can be regarded as a distributed definition for the built-in Events datatype.

Channels must also be rectangular in the same sense as used for datatypes. It is common in FDR2 to make channels finite although it is possible to declare infinite channels and use only a finite proportion of them.

Channels interact naturally with datatypes to give the functionality provided by variant channels in occam2 (and channels of variants in occam3). For example, given ComplexColour as above, we can write a process which strips out the redundant colour encodings (undoing the work performed by make_colour)

channel colour : ComplexColour
channel standard : Gun.Gun.Gun

Standardise =
    colour.RGB?x -> standard!x -> Standardise
  []
    colour.Grey?x -> standard!x.x.x -> Standardise
  []
    colour.Black -> standard!0.0.0 -> Standardise
  []
    colour.White -> standard!15.15.15 -> Standardise

A.3.6 Closure operations

Syntax

extensions(x)	the set of values which will `complete' x
productions(x)	the set of values which begin with x
{|x1 , x2|}	the productions of x1 and x2

Equivalences

productions(x) ≡	{x.z<-extensions(x) }
{| x | ...|} ≡	Union( { productions(x) | ...} )

Remarks

The main use for the ‘{| |}’ syntax is in writing communication sets as part of the various parallel operators. For example, given

channel c : {0..9}
P = c!7->SKIP [| {| c |} |] c?x->Q(x)

we cannot use {c} as the synchronisation set; it denotes the singleton set containing the channel c, not the set of events associated with that channel.

All of the closure operations can be used on datatype values as well as channels.

The closure operations are defined even when the supplied values are complete. (In that case extensions will supply the singleton set consisting of the identity value for the ‘.’ operation.)

This document was generated by Phil Armstrong on May 17, 2012 using texi2html 1.82.