Syntax sugar (Pipe-calculus)

Thoughtful application of syntax sugar makes programs easy to read, more compact and more familiar to programmers. They can even reveal nice properties of the core calculus.

Let ... in

[math]\displaystyle{ \def\seq{\mathrel{;}} \def\succeed{\textbf{succeed}} \def\alt{\mid} \def\fail{\textbf{fail}} \def\pipe{\rhd} \def\pass{\textbf{pass}} \def\in{\,?} \def\out{!} \def\rew{\mathrel{\Rightarrow}\,} }[/math][math]\displaystyle{ \mathsf{let} }[/math] is a popular construct in functional languages that declares a lexically scoped local variable. It's usual form is [math]\displaystyle{ \mathsf{let}~x = s~\mathsf{in}~t }[/math] which denotes binding the name [math]\displaystyle{ x }[/math] to the term [math]\displaystyle{ s }[/math] in the term [math]\displaystyle{ t }[/math]. In lambda calculus [math]\displaystyle{ \mathsf{let} }[/math] can be encoded as [math]\displaystyle{ (\lambda x . t)~s }[/math]. Using the [math]\displaystyle{ \beta }[/math]-rule we get [math]\displaystyle{ t[s/x] }[/math], an instance of [math]\displaystyle{ t }[/math] where [math]\displaystyle{ s }[/math] is substituted for every free occurence of [math]\displaystyle{ x }[/math]. In pipe-calculus we can do similar encoding.

[math]\displaystyle{ \mbox{Terms}~ s, t ::= ... \mid \mathsf{let}~x = s~\mathsf{in}~t }[/math]

[math]\displaystyle{ \mathsf{let}~x = s~\mathsf{in}~t \rew \out s . \fail \pipe \in x . t }[/math]

According to the defined rewriting relation, this can be rewritten as follows.

[math]\displaystyle{ \out s . \fail \pipe \in x . t \rew \fail \pipe t[s/x] \rew t[s/x] }[/math].

Arrow Syntax

Arrows makes syntax of prefixed processes more familiar to functional programmers and emphasize the connection between languages and types.

[math]\displaystyle{ \def\pto{\mathrel{\to\mkern-18mu\vcenter{\hbox{$\scriptscriptstyle|$}\mkern11mu}}} \def\nto{\to} \mbox{Terms}~ s, t ::= ... \mid a \pto s \mid a \nto s \mid s \pto t \mid x \nto s }[/math]

[math]\displaystyle{ \begin{alignat}{1} & a \pto s & \rew & ~a^+ . s \\ & a \nto s & \rew & ~a^- . s \\ & s \pto t & \rew & \,\out s . t \\ & x \nto s & \rew & \in x . s \\ \end{alignat} }[/math]

Informally, positive arrows denote outward directed operations while negative arrows denote inward directed ones. Both arrows are right associative. When it is clear from context, we can call a negative arrow simply an arrow.

Using arrow syntax and recursion we can write passNat from the introductory example like this.

[math]\displaystyle{ \mathsf{rec}~ p . (\mathsf{1} \nto \mathsf{1} \pto p \mid \mathsf{end} \nto \mathsf{end} \pto \textbf{succeed}) }[/math]