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.
Type Check File
Type System Help
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 rank1 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 builtin 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 2 2 3 4channel c : {0} 5 g :: Event 6 c.0 7 8 h :: Bool 9 true or false 10 11 P :: Proc 12 c.0 > STOP 13 14datatype X 15 k :: A 16 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> 2 <0> 3 4 n :: {Int} 5 {0} 6 7 mn  {{Int}} 8 {{i}  i < {0..}} 9 10 k :: (Int, Bool) 11 (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 2 ev > STOP 3 ev > f(n1, ev) 4 5 g :: (Int) > ((Int) > Int) > Int 6 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 B  C.{0}.Bool 3 4 c :: A=>Int=>Event 5channel c : A.{0} 6 7 p :: A.Int 8 B.0 9 10 q :: A.Int.Proc 11 C.0.true.0.STOP
Note that whilst all of the above definitions are welltyped, 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 2 = y 3 g :: Ord a => (a, a) > Bool 4 x < y 5 6 Sets require their elements to be comparable. 7 h :: Eq a => a > {a} 8 {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 Z 3 c :: Int => Event 4channel c : A 5 6 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.
10 > STOP 2 3datatype X.Int 4channel c : A 5 f(c) d?x!
Type checking this script produces the following error.
 Error <interactive>:5:78

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
Difficulties Type Checking CSPM
Note that, in general, typechecking CSPM code is undecidable. For example, consider the following program.
1{x}) x.f(
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.
About
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:5773: 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:5780: 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:19: 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 precompiled 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.