Syntax sugar (Pipe-calculus): Difference between revisions
KalmanKeri (talk | contribs) No edit summary |
KalmanKeri (talk | contribs) |
||
| Line 15: | Line 15: | ||
\def\rew{\mathrel{\Rightarrow}\,} | \def\rew{\mathrel{\Rightarrow}\,} | ||
</math> | </math> | ||
<math>\mathsf{let}</math> is a popular construct in functional languages that declares a lexically scoped local variable. It's usual form is <math>\mathsf{let}~x = | <math>\mathsf{let}</math> is a popular construct in functional languages that declares a lexically scoped local variable. It's usual form is <math>\mathsf{let}~x = s~\mathsf{in}~t</math> which denotes binding the name <math>x</math> to the term <math>s</math> in the term <math>t</math>. | ||
In lambda calculus <math>\mathsf{let}</math> can be encoded as <math>(\lambda x . | In lambda calculus <math>\mathsf{let}</math> can be encoded as <math>(\lambda x . t)~s</math>. Applying the ''<math>\beta</math>-rule'' we get <math>t[s/x]</math>, an instance of <math>t</math> where <math>s</math> is substituted for every free occurence of <math>x</math>. | ||
In pipe-calculus we can do similar encoding. | In pipe-calculus we can do similar encoding. | ||
Revision as of 22:33, 9 May 2023
Thoughtful application of syntax sugar makes programs easy to read, more compact and more 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 = 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]. Applying 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 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]
Intuitively a positive arrow denotes outward directed operations and negative arrow denotes inward directed ones. [1] Both arrows are right associative. When it is clear from context, we can call a negative arrow simply an arrow.
Notes
- ↑ Notice that the arrow syntax is unambiguous because variables can always be distinguished from atoms and an atom without a polarity does not occur anywhere else in the syntax.