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.

History

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.

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.

*all?t. { take!t | skip!t } | *case take? of { Leaf ⇒ {} ; Node(c,l,r) ⇒ c!3 | take!l | skip!r } | *case skip? of { Leaf ⇒ {} ; Node(c,l,r) ⇒ skip!l | take!r } | all!tree

The types inferred by Hypha reflect the behavior of the three processes:

all : {ω,1}[μα.(Leaf ⊕ Node {0,1}[Int] × α × α)] take : {ω,ω}[μα.(Leaf ⊕ Node {0,1}[Int] × α × μβ.(Leaf ⊕ Node {0,0}[Int] × β × α))] skip : {ω,ω}[μα.(Leaf ⊕ Node {0,0}[Int] × α × μβ.(Leaf ⊕ Node {0,1}[Int] × β × α))] tree : μα.(Leaf ⊕ Node {0,1}[Int] × α × α)

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.

*server?s. case s? of { Quit ⇒ {} ; Plus c1 ⇒ c1?(x,c2).c2?(y,c3).new c4 in { c3!(x + y, c4) | server!c4 } ; Eq c1 ⇒ c1?(x:Int,c2).c2?(y,c3).new c4 in { c3!(x = y, c4) | server!c4 } ; Neg c1 ⇒ c1?(x,c2).new c3 in { c2!(0 - x, c3) | server!c3 } }

Below is the type of server inferred by Hypha when using the -s option, which activates the decompilation of linear types into session types:

server : {ω,ω}[μα.?{Eq : ?[Int].?[Int].![Bool].α, Neg : ?[Int].![Int].α, Plus: ?[Int].?[Int].![Int].α, Quit: end}]

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.

{ { *node?(%val). split %val as %1 : [0,0], %2 : [0,0] in let x : [0,0] = %1 : [0,0] in let y : [0,0] = %2 : [0,0] in new a : [1,3] in { x : [0,0]!a : [1,2] | y : [0,0]?(z : [1,1]).node!(a : [1,1] , z : [1,1]) } | node!(e : [0,1] , f : [0,1]) } | node!(f : [0,1] , e : [0,1]) }

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] [. Process] output
| Expression?[Pattern] [. Process] input
| let Pattern = Expression in Process local binding
| def Definition [and Definition]* in Process definitions
| case Expression [?] of { Rule [; Rule]* } pattern matching
| if Expression then Process else Process conditional
| Process | Process parallel composition
| new var [: Type] in Process new channel
| { [Process] } group
| *Process replication
Definition ::= var?[Pattern] = Process persistent input
Rule ::= tag [Pattern] ⇒ Process match
Pattern ::= () unit
| _ [: Type] anonymous
| var [: Type] variable
| Pattern as var [: Type] ascription
| 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