Syntax sugar (Pipe-calculus)

Thoughtful application of syntax sugar makes programs easy to read, more compact and familiar to programmers. The syntax extensions described here are lightweight and well-defined.

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 = t~\mathsf{in}~u }[/math] which denotes binding the name [math]\displaystyle{ x }[/math] to the term [math]\displaystyle{ t }[/math] in the term [math]\displaystyle{ u }[/math]. In lambda calculus [math]\displaystyle{ \mathsf{let} }[/math] can be encoded as [math]\displaystyle{ (\lambda x . u)~t }[/math]. Applying the [math]\displaystyle{ \beta }[/math]-rule we get [math]\displaystyle{ u[t/x] }[/math], an instance of [math]\displaystyle{ u }[/math] where [math]\displaystyle{ t }[/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 brought to a normal form in two steps.

[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]

The new operators are called positive arrow and negative arrow respectively. They are right associative like the function arrow normally is. When it is clear from context, we can call a negative arrow simply an arrow.