To type check a file copy and paste the source into the area below. Please note, include statements are not supported in the web based version.

  1. Type System
    1. Ground Types
    2. Constructor Types
    3. Channels and Datatypes
    4. Type Constraints
  2. Common Errors
  3. Type Checking Difficulties

The type system used in libcspm is very essentially a simplified version of Haskell's, along with suitable modifications to enable processes and events to be represented. More formally, it is a rank-1 polymorphic type system, meaning that polymorphic functions (like id(x) = x) can be defined, but any universal quantifications must be on the outside.

In this section we give a brief overview of the type system and then give several examples to show how some of the most common errors present in CSPM scripts can be detected. Lastly, we explain some of the difficulties involved in type checking CSPM, and explain why it is, in general, undecidable.

The Type System

In this section we present the type system, along with several examples to illustrate it. Throughout this section we write f :: t to mean that f is of type t. We write type variables using lowercase letters, like a.

The Ground Types

The built-in ground types are consist of type variables, like a along with Bool, Event, Int and Proc, which represent the type of booleans, events, integers and processes respectively. There is also a special type, Eventable, that represents something that is either an Event, or which can be made into an event by dotting it with suitable values. For example, in the expression {| c |}, c is merely required to be Eventable.

As CSPM allows the user to define new datatypes, ground types can be defined within the users source. For example, if the user writes datatype A = ... within their file, then a new ground type A is defined.

The example below contains some variables that are of ground types. Each variable's type is given on the line above.

   1-- f :: Int
   2f = 2
   3
   4channel c : {0}
   5-- g :: Event
   6g = c.0
   7
   8-- h :: Bool
   9h = true or false
  10
  11-- P :: Proc
  12P = c.0 -> STOP
  13
  14datatype  A = X
  15-- k :: A
  16k = X

Constructor Types

Type constructors take a type argument, and then return a new type. In CSPM the simple type constructor are <a>, {a} and (a,b,c,...,z), representing something of type list of a, set of a, or a tuple of values. For example, consider the following.

   1-- m :: <Int>
   2g = <0>
   3
   4-- n :: {Int}
   5n = {0}
   6
   7-- mn -- {{Int}}
   8mn = {{i} | i <- {0..}}
   9
  10-- k :: (Int, Bool)
  11k = (0, true)

There is also a function constructor type. We say f has type (a,b,c) -> d iff f takes 3 arguments, of type a, b and c respectively, and returns something of type d. For example, consider the following.

   1-- f :: (Int, Event) -> Process
   2f(0,ev) = ev -> STOP
   3f(n,ev) = ev -> f(n-1, ev)
   4
   5-- g :: (Int) -> ((Int) -> Int) -> Int
   6g(n)(h) = h(n)

Note that, so far, the type system is exactly like Haskell's, just with a slightly different syntax and a couple of different ground types.

Channels and Datatypes Or How Dot Causes Problems

We now consider how to type channels and datatypes. Suppose, for instance, that we have the following channel declaration and consider what type we might assign to c.

   1channel c : {0}

Observe that when c is placed on the left of a variable, say x that is of type Int, (i.e. as in c.x) then it yields something of type Event. Therefore, this suggests the type of c should be “something that, when dotted (i.e. placed on the left of a dot) with something of type Int, yields an event”. Therefore, we introduce a new type constructor, yields, written =>, and say that c is of type Int => Event (pronounced “c is of type Int yield Event”).

This lets us type almost any CSPM program, with one particular exception. Consider the expression 0.0; this is perfectly valid, and whilst not in general advisable, it can be useful under certain circumstances. Therefore, we introduce one further type constructor, dot. If something is of type t1.t2 then it consists of two things dotted together, where the left hand side is of type t1 and the right hand side is of type t2.

We now consider several examples of the above.

   1-- B :: A, C :: Int=>Bool=>A
   2datatype  A = B | C.{0}.Bool
   3
   4-- c :: A=>Int=>Event
   5channel c : A.{0}
   6
   7-- p :: A.Int 
   8p = B.0
   9
  10-- q :: A.Int.Proc
  11q = C.0.true.0.STOP

Note that whilst all of the above definitions are well-typed, some of them (in particular p and q) are inadvisable and may be rejected by a future, stricter, type checker. For further discussion see the section on difficulties with type checking.

Constraints

Like in Haskell we allow type variables to be constrained in certain ways. In general, if a type variable a has a constraint c then a may only be instantiated with types that satisfy the constraint c.

There are three possible constraints on type variables: Eq, Ord and Inputable. If a type variable a has the constraint Eq a, then this means that the type variable can be anything, providing equality is defined for values of type a. For example, this means that the type Int would be admissible, but no function types would be as functions are not comparable.

A type t satisfies the constraint Ord when the type represents something that can be ordered (i.e. using < or similar). For example, Int satisfies the constraint Ord, but functions or processes would not.

As an example of these consider the following.

   1-- f :: Eq a => (a, a) -> Bool
   2f(x,y) =  x == y
   3-- g :: Ord a => (a, a) -> Bool
   4g(x,y) = x < y
   5
   6-- Sets require their elements to be comparable.
   7-- h :: Eq a => a -> {a}
   8h(x) = {x}
   9
  10-- This would be allowed, as Int satisfies Eq.
  11f(0,1)
  12-- This would be allowed, as Int satisfies Ord.
  13g(0,1)
  14-- These would not be allowed, as no function type satisfies Eq or Ord.
  15f(f, g)
  16g(f, g)

The last type variable constraint is more complicated, and appears only very rarely. We say that a type t satisfies the constraint Inputable a if it is not a yield type. To see why this is necessary consider the following example.

   1-- Z :: A
   2datatype  A = Z
   3-- c :: Int => Event
   4channel c : A
   5
   6f(X) = c?x:X!0 -> STOP

When evaluating c?x!0, the evaluator has to pick a set of elements for x to range over. Therefore, as c has only one channel component, of type A, this set would need to consist of elements of type Int=>A (as then x.0 would be of type A, as required). However, the rules that the evaluator uses for picking this set essentially say that it matches one field. Therefore, in the above example, x would range over everything of type A.

For example, consider the following script.

   1f(d) = d?x!0 -> STOP
   2
   3datatype  A = X.Int
   4channel c : A
   5g = f(c)

Type checking this script produces the following error.

Error <interactive>:5:7-8
The type Int=>A does not have the constraint Inputable
In the first argument of f, namely c
In the expression: f(c)
In a pattern binding: g = f(c)

Common Errors

Forthcoming.

Difficulties Type Checking CSPM

Presently incomplete.

Note that, in general, typechecking CSPM code is undecidable. For example, consider the following program.

   1f(x) = x.f({x})

Clearly f is well typed. Consider the type of f; clearly f takes one argument, say of type a. However, the value it returns is of type a.{a}.{{a}}.... Hence, this function's type is necessarily infinite.

This webpage makes use of the typechecker provided by libcspm. This package provides two commands, cspmchecker and cspmcheckeri. The first, cspmchecker simply takes a list of files and then prints any type errors to the console. The following example illustrates its usage.

$ cspmchecker burglar.csp 
Checking burglar.csp.....
./burglar.csp:225:57-73:
    Couldn't match expected type (({(Identifiers, Int)}, a, b)) -> (<Int>, <needs>)
            with actual type (({(Identifiers, Int)}, c, d)) -> (Int, <needs>)>
    In the second argument of snocf, namely <Ival(lastdigs)>
    In the expression: snocf(Ival(key), <Ival(lastdigs)>)
    In the expression: (lastdigs, snocf(Ival(key), <Ival(lastdigs)>))

./statechartcompiler.csp:124:57-80:
    Couldn't match expected type {a} with actual type ({Int}, b)
    In the first argument of Set, namely (Statelabel, Statechart)
    In the expression: Set((Statelabel, Statechart))
    In the expression: Set(ActLabel).Set((Statelabel, Statechart))

The second command, cspmcheckeri, provides an interactive environment, much like ghci or hugs. The following example shows some of the functionality available.

$ cspmcheckeri
> :load phils.csp 
Ok, loaded phils.csp
phils.csp> 
ASPHILS    AlphaF     FORK       LPHILs     PHILS      SYSTEMs    picks
ASPHILSs   AlphaP     FORKNAMES  N          PHILs      T          putsdown
ASSYSTEM   BSYSTEM    FORKS      PHIL       SYSTEM     eats       sits
ASSYSTEMs  BUTLER     LPHIL      PHILNAMES  SYSTEM'    getsup     thinks
phils.csp> :type PHIL
PHIL :: (Int) -> Proc
phils.csp> :type thinks
thinks :: Int=>Event
phils.csp> PHIL(0)
PHIL(0)
phils.csp> :
:load       :printProc  :quit       :reload     :type
phils.csp> :printProc PHIL(0)
PHIL(0) =
thinks.0 -> sits.0 -> picks.0.0 -> picks.0.1 -> eats.0 -> putsdown.0.1 -> putsdown.0.0 -> getsup.0 -> PHIL(0)

PHIL(0)
phils.csp> :printProc eats.0.0 -> STOP
<interactive>:1:1-9:
Couldn't match expected type Int with actual type Int.Int
whilst matching expected type Event with actual type Event.Int
In the expression: eats.0.0
In the expression: eats.0.0 -> STOP

These tools can either be installed by downloading a pre-compiled binary from here, however, the recommened route is to install using Cabal, the Haskell package manager. This can be done by firstly installing the Haskell Platform (ensuring that GHC is at least version 7), then by running cabal install cspmchecker on the command line.

Credits

This website makes use of libcspm, the Snap Framework, Twitter Bootstrap and Solarized. Source code available from GitHub.