Hypha - Type Reconstruction for the Linear π-Calculus
Hypha is a proof of concept implementation of the type reconstruction algorithm described in Type Reconstruction for the Linear π-Calculus with Composite and Equi-Recursive Types. It is implemented in Haskell, comes with the full source code (see the download section below) and a bunch of examples.
- Release history
- Download the source code
- Have a look at the syntax of processes accepted by Hypha
- Check out some references on the linear π-Calculus
History
- 4 Jan 2016: released version 0.6 with performance improvements.
- 10 Nov 2015: profiling has revealed two major performance bottlenecks in the pretty printing of large processes and during deadlock freedom analysis. Both have been successfully addressed.
- 6 Dec 2014: first release with support for deadlock and lock freedom analyses.
- 15 Sep 2014: implemented decompilation of linear types into session types. Almost ready to release deadlock and lock analysis, but the code has been commented out and omitted from this release.
- 13 Aug 2014: the internals of Hypha have been completely reworked. Hypha now implements an efficient use resolution algorithm, disjoint sums have been replaced by variant types, and the syntax of processes has been revised. Lots of new interesting examples can be typed!
- 29 Nov 2013: added support for fst and snd operators as suggested by one of the FoSSaCS reviewers; generalized syntax for sends and receives, now the subject can be an arbitrary expression.
- 30 Aug 2013: initial release.
Download
The source code of Hypha can be downloaded at the links below. For versions up to (and including) 0.4, you need GHC, Alex and Happy to compile the tool. The easiset way to get them all at once is to install the Haskell Platform. In addition, you must install the Haskell packages base-unicode-symbols, containers-unicode-symbols, and multiset. A Makefile is provided.
Starting from version 0.5, you also need GLPK and the corresponding Haskell binding glpk-hs. Work is in progress to make this dependency optional.
- hypha 0.6 [.tar.gz]
- hypha 0.5 [.tar.gz]
- hypha 0.4 [.tar.gz]
- hypha 0.3 [.tar.gz]
- hypha 0.2 [.tar.gz]
- hypha 0.1 [.tar.gz]
Examples
Below are three processes that visit a binary tree where each node contains a channel: take sends a message on the channel found on any node that is reachable through an even number of right branches from the root of the tree; skip sends a message on the channel found on any node that is reachable through an odd number of right branches from the root of the tree; overall, all sends a message on every channel in the tree.
The types inferred by Hypha reflect the behavior of the three processes:
Next is a process that models a server accepting requests for various mathematical operations. The server is modeled using the continuation-passing style that is implicit in session-based models.
Below is the type of server inferred by Hypha when using the -s option, which activates the decompilation of linear types into session types:
Since version 0.5 Hypha is capable of performing deadlock and lock freedom analyses as described in the paper Deadlock and Lock Freedom in the Linear π-Calculus. Below is the result of Hypha's lock freedom analysis on the full duplex communication example full_duplex.hy included in the source archive. The numbers in square brackets respectively denote the level and the tickets associated with channels. The existence of these annotations means that the program is lock free. Note the use of polymorphic recursion in the invocations of node.
Syntax
Below is the EBNF grammar describing the syntax of processes accepted by Hypha. The symbols ⇒ ≤ ≥ ≠ × ∧ ∨ ¬ can also be entered as => <= >= <> * /\ \/ not respectively.
Process | ::= | Expression! | Expression . Processoutput |
| | Expression? | Pattern . Processinput | |
| | let Pattern = Expression in Process | local binding | |
| | def Definition | and Definitiondefinitions | |
| | case Expression | ? of { Rule ; Rule }pattern matching | |
| | if Expression then Process else Process | conditional | |
| | Process | Process | parallel composition | |
| | new var | : Type in Processnew channel | |
| | { | Process }group | |
| | *Process | replication | |
Definition | ::= | var? | Pattern = Processpersistent input |
Rule | ::= | tag | Pattern ⇒ Processmatch |
Pattern | ::= | () | unit |
| | _ | : Typeanonymous | |
| | var | : Typevariable | |
| | Pattern as var | : Typeascription | |
| | Pattern, Pattern | pair | |
| | (Pattern) | group | |
Expression | ::= | () | unit |
| | n | integer | |
| | true | boolean true | |
| | false | boolean false | |
| | var | variable | |
| | unop Expression | unary operator | |
| | Expression binop Expression | binary operator | |
| | (Expression) | group | |
Type | ::= | Unit | Bool | Int | basic types |
binop | ::= | ∧ | ∨ | < | > | ≤ | ≥ | = | ≠ | + | - | × | / | , | binary operators |
unop | ::= | tag | ¬ | fst | snd | unary operators |
var | ::= | a-z a-z 0-9 _ ' | variable |
tag | ::= | A-Z a-z 0-9 _ ' | tag |
n | ::= | 0-9 | integer |
References
- Luca Padovani, Deadlock and Lock Freedom in the Linear π-Calculus, in Proceedings of CSL-LICS 2014.
- Luca Padovani, Type Reconstruction for the Linear π-Calculus with Composite and Equi-Recursive Types, in Proceedings of FoSSaCS 2014.
- Atsushi Igarashi, Naoki Kobayashi, Type Reconstruction for Linear π-Calculus with I/O Subtyping, Information and Computation, 161(1):1-44, 2000
- Naoki Kobayashi, Benjamin C. Pierce, David N. Turner, Linearity and the pi-calculus, ACM Transactions on Programming Languages and Systems, 21(5):914-947, ACM, 1999