One of the new features of FDR3 is a builtin type-checker. The type-checker is not complete in that it will reject some programs that are correctly typed, but permits virtually all reasonable CSP_{M} scripts. In this section we document the type system, starting with the type atoms, then documenting the constructed types before lastly documenting the type constraints.
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.
Char
¶The type of characters. All Unicode (or equivalently ISO/IEC 10646) characters are supported.
Datatype
n¶The type of a user defined datatype. For example, given the following:
datatype X = Y.{0..1} | Z
then Z ::
and n
Y.0 ::
. n
Event
¶The type of fully constructed events. For example, given the following definitions:
channel c : {0..1}
channel done
Int
¶The type of integers. This is defined as supporting values between \(-2^{31} +1\) and \(2^{31} -1\), inclusive.
Dot
a.b¶The type of two items x ::
and a
y ::
that have
been combined together using the dot operator. For example, b
1.1 ::
.
Int
.
Int
Dotable
a => b¶If x ::
then a => b
can be dotted with something of
type x
to yield a value of type a
. Thus, if
b
y ::
then a
x.y ::
. This type is used in channel
and datatype declarations as follows: b
channel c : Int.Int
datatype X = Y.Int.Bool
Extendable
a =>* b¶A value of type
is something that can be extended to a
value of type a =>* b
. In particular, it is either of type
b
, or is something of type b
. Note that if
something is of type a => b
then a =>* b
is guaranteed to
be an atomic type variable and a
will satisfy
b
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}
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 ::
and (
Int
,
Int
) ->
Int
singleton :: (
.Set
a) => (a) -> {a}
Map
(| k => v |)¶The type of a map from type k
to type v
.
New in version 3.0.
Sequence
<a>¶The type of sequences where each element is of type a
.
Set
{a}¶The type of sets that contain items of type a
. Constructing a set
requires the inner type to satisfy Set
.
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
.
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.
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
.
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
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.
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.
Dot
(right-associative)Dotable
, Extendable
(all right-associative)