A concurrent programming language with a linear type and effect system
A concurrent programming language with a linear type and effect system
Lollyscript is a concurrent programming language. On this page, we will explain the basics of LollyScript, its linearity and how we use a linear type system to guarantee that promises will be resolved. You can find a more elaborate tutorial on LollyScript here. All examples (and changes to it) can be run.
Programming in LollyScript is very straightforward. The basic language constructs of LollyScript include: let, letrec, lambdas, pairs and records, sum types and variants, and algebraic data types. The following code example displays the "hello world" of LollyScript.
Records can be constructed using curly braces. You can deconstruct the record using the let construct.
LollyScript has support for linear types, based on linear logic. With linear types the programmer can ensure that his resources are used exactly once. In LollyScript a linear type or value is indicated with "§" or "lin". For example a linear type int is denoted as §int or lin int. Similarly, values can also be made linear using "§" or "lin", for example lin 5 or §5. Types and values are default unrestricted (normal). You can indicate this using un, but this is not required.
The code example below shows a lambda (f) that expects a linear integer as argument. Note that x is used exactly once in the body of the lambda. In the body of the let construct, we call f with a linear 5 as argument.
A promise is a language construct often used in concurrent programming languages. It is a placeholder for a value that will be known later. For more information on promises, check the wiki page.
In LollyScript, promises exist out of two parts: a future (used for reading the value of the promise) and a resolver (used to set the value of the promise). A promise can be constructed using the Promise function. This function expects three arguments:
It returns a record of two elements: the first one is the future and the second one is the resolver. The future is used to read the value of a promise, and the resolver is used to write the value of the promise. A promise can be written to using resolve: it expects a resolver and a value. Reading the value of a promise can be done synchronously (by calling wait with a future) and asynchronously (using listen which, next to the future, also expects a listener).
The type system of LollyScript statically detects that a promise is not resolved, even when this is due to the blocking wait construct which causes the program to hang. LollyScript also takes into account the different processes in which expressions are executed.
You can find more examples of promises on the home page.