# Typecheker and Interpreter for Language CLASS This document describes how to use the type checker and interpreter for language CLASS. The language foundations are described in the paper "Typeful Concurrent Programming with CLASS" Authors: Luis Caires and Pedro Rocha [![CC BY 4.0][cc-by-shield]][cc-by] This work is licensed under a [Creative Commons Attribution 4.0 International License][cc-by]. [![CC BY 4.0][cc-by-image]][cc-by] [cc-by]: http://creativecommons.org/licenses/by/4.0/ [cc-by-image]: https://i.creativecommons.org/l/by/4.0/88x31.png [cc-by-shield]: https://img.shields.io/badge/License-CC%20BY%204.0-lightgrey.svg ## Getting Started The directory should have the following contents: * `README.md` -- This file. * `LICENSE.txt` -- Creative Commons Atrribution 4.0 International License. * `bin/` -- Folder containing the compiled Java .class files. * `examples/pure` -- Folder containing examples involving only pure computations (without state). * `examples/state` -- Folder containing examples involving shared state. * `lib/` -- Folder containing boot definitions loaded by the interpreter. * `src/` -- Folder containing the Java source files. * `CLLSj` -- Executable file to start the interactive REPL. * `makeit` -- Executable file that compiles the source code. To compile the source code execute `./makeit`. To run the interpreter as an interactive REPL execute `./CLLSj`. We recommend starting with three basic examples, which are commented and built step-by-step * `examples/pure/arithmetic-server.clls` * `examples/state/first-class-cells.clls` * `examples/state/simple-counter-lin.clls` Examples come with several tests, mostly on the shared concurrent ADTs. For example, to try the imperative queue type the following ``` include "examples/state/imperative-queue/tests.clls";; systemPar();; ``` After including the necessary definitions, this file runs two concurrent processes: one enqueues the integers from 1 to 300 and, the other dequeues 300 elements from the queue. ## Interacting with the REPL (read-eval print loop) The REPL expects the following top-level commands: 1. type id(X1,...,Xn){ A };; 2. type rec id(X1,...,Xn){ A };; 3. type corec id(X1,...,Xn){ A };; 4. proc id(x1:A1, ... xm:Am ; y1:B1, ..., yk:Bk){ P };; 5. proc rec id(x1:A1, ... xm:Am ; y1:B1, ..., yk:Bk){ P };; 6. proc unsafe_rec id(x1:A1, ... xm:Am ; y1:B1, ..., yk:Bk){ P };; 7. P;; 8. trace P;; 9. include "filename";; 10. quit;; Command (1): top level type definition. Defines (if it kindchecks) the (possibly) parametric type A with name id and parameters X1, ... Xn ( n >= 0). Example: > type fun(a,b) { recv ~ a; b };; Type fun: defined. Command (2) and (3) are similar to (1) but allows inductive (mu X. A) and coinductive (nu A. A) type definitions, respectively. For example, > type rec Nat{ choice of { |#Z: close |#S: Nat } };; defines the recursive session type of the natural numbers. (4) Defines (if it typechecks) the (possibly) parametric process with name id with linear parameters x1:A1,..., xm:Am (m >0) and unrestricted (exponential) parameters y1:B1,..., yk:Bk (k>=0). The process is typechecked as defined by the typing judgment P |- x1:A1,..., xm:Am ; y1:B1,..., yk:Bk Example: > proc id(f:fun(a,a)) { recv f (x:~a);fwd x f } ;; Process id: defined. Command (5) is same as (4) but allows corecursive process definitions, e.g.: > proc rec double(n:~Nat, m:Nat) { case n of { |#Z: wait n; zero(m) |#S: cut{ double(n,k) |k:~Nat| #S m; #S m; fwd m k } } };; defines a corecursive process that doubles natural `n` and outputs the answer on `m`.The type checker ensures each that corecursive call is done in a session that hereditarily descends from the corecursion parameter. Command (6) allows to define an unsafe corecursion definition, in which the herediraty check of (5) is turned off. Commands (7) and (8) typecheck process P in the current environment given by prior definitions and execute it, (6) with tracing enabled. Example: > cut { id(f) |f:~fun(lint,lint)| send f (x:~colint. let x 10); println "here is "+f; () };; here is 10 Command (9) includes and processes all the commands included in the specified file. Filename are given as strings. Example: > include "examples/tests/stack";; Command (10) quits the REPL. Single-line comments are written as follows //this is a single-line comment whereas multiple-line comments are written as /* this is a multiple-line comment */ By convention, we use the filename extension `.clls` for files written in the implementation language. ## Concrete Syntax The concrete syntax of types is given by:: A,B ::= lint | colint | lbool | colbool | lstring | colstring | close | wait | send A; B | ( A (x) B ) recv A; B | ( A (p) B ) choice of {|#l1:A1 | ... |#ln: An} | ( (+){|#l1:A1 | ... |#ln: An} ) offer of {|#l1:A1 | ... | #ln:An} | ( &{|#l1:A1 | ... |#ln: An} ) !A | ?A | sendty X; A | ( Exists X. A ) recvty X; A | ( Forall X. A ) affine A | (/\ A) coaffine A| (\/ A) state A | (Sf A) usage A | (Uf A) statel A | (Se A) usagel A | (Ue A) { A }  | id(A1,...,An) The correspondence to the types of the paper are written in parenthesis. Except for the basic type constants, concrete types correspond to the types described in the paper. We have basic type constants for linear integers `lint`, linear booleans `lbool`and linear strings `lstring`, as well as their dual `colint`, `colbool` and `colstring`. Unrestricted versions of these types may be defined using ! and ? type constructors. Choice label identifiers must start by a hash character`#`. The concrete syntax of process terms is given by:: P, Q ::= print M; P | println M; P | if M { P } { Q} | let x M | let! x M | id(x1, ..., xm) | () | par {P || Q } | share x { P || Q } | fwd x y | cut { P |x:A| Q } | close x | wait x; Q | case x of {|#l1:P1 | ... | #ln:Pn} | #li;Pi | send x(y:A. P); Q | recv x(y:A);Q | !x(y:A);P | call x(y:A);P | ?x; P | sendty x(A);P | recvty x(X);P | send x(M);P | affine x; P | use x; P | discard x | take x(y:A);P | put x(y:A. P); Q | put x(M);P | cell x(y:A. P) | cell x(M) | release x | Construct `id(x1,.. ; .,xm)` spawns the defined process `id` with type arguments "A1,..., An and channel name arguments `x1,..; .,xm`. The `;` in the argument list separates the linear parameters from the unrestricted parameters, according to the definition of id. Except for the first five lines, which refer to expressions for basic datatypes, described in more detail below, all the constructs of the concrete process syntax are the fundamental ones introduced in our paper. Access to affine (via use process construct) and exponential names (via why-not ? process construct) is inferred by our type checker, so it does not need to be explicitly indicated. Process `print M ; P` prints message `M` and continues as `P`. Process `println M;P` prints message `M`, starts a newline, and continues as `P`. Process `if M { P } { Q }` evaluates boolean expression `M`. If the result is `true`, it continues as `P`. Otherwise, the result is `false` and it continues as `Q`. We support ML-style let-bindings. Construct `let x M` binds expression `M` to channel `x` to be used linearly (type as either `lint`, `lbool` or `lstring`). Construct `let! x M` binds expression `M` to channel `x` to be used persistently (typed as either `!lint`, `!lbool` or `!lstring`). The concrete syntax of basic value expressions is given by:: M :: = n | true | false | str | x | (M) | -M | M + M | M - M | M * M | M / M | !M | M and M | M or M | M == M | M != M | M < M | M > M where `n` is any integer, `true` and `false` denote the boolean constants, `str` is any string and `x` is an identifier. We support the usual arithmetic operations of negation, addition, subtraction, multiplication and division. We support the boolean constructs of logical negation `!`, logical `and` and logical `or`. We can compare two expressions for value equality `==` and non-equality `!=`. We can compare two integers with the usual relational operators "<" and ">". The operator of addition `+` is overloaded: we can concatenate two string expressions, obtaining a string. We can also concatenate a string with an integer expression, in which case, the integer is first converted to a string. We also provide support for expressions in the constructs send, cell and put: send x(M);P cell x(M) put x(M);P The elaboration phase of our interpreter expands this in the basic language before typechecking,. For convenience, our concrete syntax supports multi-ary par and multi-ary cut (which are abbreviations of the expected associative composition of par and cut). `par {P1 || ... || Pn}` `cut { P1 |x1:A1| ... |xn:An| Pn+1}` Multi-ary cut associates (conventionally) to the right. ## Type inference ## Differences from the core language in the paper In our concrete process syntax terms are written with bound names type-annotated, which from a pragmatic point of view guides the typechecking algorithm and eases the task of writing programs. Currently, inference of annotations is provided, so that only parameters in process definitions and cut bound names need to be explicitly type annotated. The supported language also includes pragmatic extensions (native basic datatypes int, boolean and string), that may be anyway encoded in our the fundamental linear logic based language using recursive/corecursive session types. ### Remarks about the implementation internals The system is written in the Java programming language, and all concurrency is implemented using java.util.concurrent package. The performance is quite reasonable for a proof of concept, since it heavily relies on fine-grained concurrency and programs may create many threads.