Type System¶

Type Atoms¶

type a¶

A type variable that represents some type. Like variables, these must begin with an alphabetic character and are followed by any number of alphanumeric characters or underscores optionally followed by any number of prime characters ('). There is no limit on the length of type variables and case is significant.

type Bool¶

The type of boolean values, i.e. True and False.

type Char¶

The type of characters. All Unicode (or equivalently ISO/IEC 10646) characters are supported.

type Datatype n¶

The type of a user defined datatype. For example, given the following:

datatype X = Y.{0..1} | Z

then Z :: n and Y.0 :: n.

type Event¶

The type of fully constructed events. For example, given the following definitions:

channel c : {0..1}
channel done

then c.0 :: Event and done :: Event.

type Int¶

The type of integers. This is defined as supporting values between \(-2^{31} +1\) and \(2^{31} -1\), inclusive.

type Proc¶

The type of constructed processes, such as STOP.

Type Constructors¶

type Dot a.b¶

The type of two items x :: a and y :: b that have been combined together using the dot operator. For example, 1.1 :: Int.Int.

type Dotable a => b¶

If x :: a => b then x can be dotted with something of type a to yield a value of type b. Thus, if y :: a then x.y :: b. This type is used in channel and datatype declarations as follows:

channel c : Int.Int
datatype X = Y.Int.Bool

In the above, c :: Int=>Int=>Event and Y :: Int=>Bool=>X.

type Extendable a =>* b¶

A value of type a =>* b is something that can be extended to a value of type b. In particular, it is either of type b, or is something of type a => b. Note that if something is of type a =>* b then a is guaranteed to be an atomic type variable and b will satisfy Yieldable. This type most commonly appears in the context of enumerated sets. For example if f(x) = {|x|} then f :: (Yieldable b) => (a=>*b) -> {b}.

type Function (C_1 a_1, C_2 a_2, …) => (a_1, a_2, …, a_n) -> b¶

The type of a function that takes n arguments of type a_1, a_2, respectively, each of which satisfies the appropriate type constraints C_1, C_2 etc, and returns something of type b. For example, given the following definitions:

plus(x, y) = x + y
singleton(x) = {x}

then plus :: (Int, Int) -> Int and singleton :: (Set a) => (a) -> {a}.

type Map (| k => v |)¶

The type of a map from type k to type v.

New in version 3.0.

type Sequence <a>¶

The type of sequences where each element is of type a.

type Set {a}¶

The type of sets that contain items of type a. Constructing a set requires the inner type to satisfy Set.

type Tuple (a_1, a_2, …, a_n)¶

Something of type (a_1, a_2, ..., a_n) is a tuple where the i^th item is of type a_i.

Type Constraints¶

type constraint Eq¶

A type satisfying Eq can be compared using ==. All of the type atoms except for Proc satisfy Eq, although Datatype only satisfies Eq if every field satisfies Eq. For example, if Z was a datatype defined as datatype Z = A.Proc | B.Int, then Z would not satisfy Eq as Proc does not. All constructed types, except for Function, satisfy Eq providing their type arguments do so.

type constraint Complete¶

A type satisfying Complete is something that is not of the type a => b. That is, it represents a value that cannot be extended to a datatype or channel by applying Dot.

type constraint Ord¶

A type satisfying Ord can be compared using <, <=, >= and >. Of the type atoms, only Char and Int satisfy Ord. Of the constructed types, Map, Sequence, Set and Tuple satisfy Ord providing all their type arguments satisfy the type constraint Eq (bold not Ord).

See also

Comparison

for more details on the ordering relation that each type uses.

type constraint Set¶

This indicates that a type variable must be something that sets can contain. Any type that satisfies Eq also satisfies Set but, in addition, Proc also satisfies Set. Further, All constructed types, except for Function, satisfy Set providing their type arguments do so.

Other functional languages do not generally require such a type constraint, as their set implementations merely require that items are comparable using Eq, and possibly Ord. In CSP_M this is not an option as processes are not comparable, but it is often useful (and indeed necessary) to construct sets of processes.

Note that some of the set functions require the set to contain items that satisfy Eq. This is done to prevent the equality of two processes being checked via other means, such as via the function areEqual(p1, p2) = card({p1, p2}) == 1, which checks if p1 and p2 are equal.

type constraint Yieldable¶

This type constraint is satisfied only by Event and Datatype. It indicates that the type variable must be something that can be yielded by dotting together several values.

Binding Strength¶

The binding strength for the CSP_M type constructors is given below as a list of the constructors in descending order of binding strength (i.e. items higher in the list bind tighter). Multiple entries on a single level means that the operators have equal binding strength, meaning that brackets may be necessary to disambiguate the meaning. The associativity of the operators is given in brackets.

1. Dot (right-associative)
2. Dotable, Extendable (all right-associative)