Syntax sugar (Pipe-calculus): Difference between revisions
KalmanKeri (talk | contribs) |
KalmanKeri (talk | contribs) |
||
| (7 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
Thoughtful application of syntax sugar makes programs easy to read, more compact and more familiar to programmers. | 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 == | == Let ... in == | ||
| Line 6: | Line 5: | ||
<math> | <math> | ||
\def\seq{\mathrel{;}} | \def\seq{\mathrel{;}} | ||
\def\alt{\mid} | \def\alt{\mid} | ||
\def\pipe{\rhd} | \def\pipe{\rhd} | ||
\def\pass{\textbf{pass}} | \def\pass{\textbf{pass}} | ||
| Line 14: | Line 11: | ||
\def\out{!} | \def\out{!} | ||
\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 = 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>. | ||
<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 . t)~s</math>. Using 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 lambda calculus <math>\mathsf{let}</math> can be encoded as <math>(\lambda x . t)~s</math>. | |||
In pipe-calculus we can do similar encoding. | In pipe-calculus we can do similar encoding. | ||
| Line 24: | Line 20: | ||
<math> | <math> | ||
\mathsf{let}~x = s~\mathsf{in}~t \rew \out s . \ | \mathsf{let}~x = s~\mathsf{in}~t \rew \out s . \bot \pipe \in x . t | ||
</math> | </math> | ||
Using the defined [[Pipe-calculus#Normal_forms|rewriting relation]], this can be rewritten as follows. | |||
<math>\out s . \ | <math>\out s . \bot \pipe \in x . t \rew \bot \pipe t[s/x] \rew t[s/x]</math>. | ||
== Arrow Syntax == | == Arrow Syntax == | ||
| Line 52: | Line 48: | ||
</math> | </math> | ||
Informally, '''positive arrows''' denote outward directed operations while '''negative arrows''' denote inward directed ones. | |||
<ref> | <ref> | ||
The arrow syntax is unambiguous because variables can always be distinguished from atoms and an atom without polarity does not occur anywhere else in the syntax. | |||
</ref> | </ref> | ||
Both arrows are right associative. | Both arrows are right associative. | ||
When it is clear from context, we can call a negative arrow simply an arrow. | When it is clear from context, we can call a negative arrow simply an arrow. | ||
Using arrow syntax and recursion we can write <code>passNat</code> from the [[Pipe-calculus#An_example|introductory example]] like this. | |||
<math>\mathsf{rec}~ p . (\mathsf{1} \nto \mathsf{1} \pto p \mid \mathsf{end} \nto \mathsf{end} \pto \top)</math> | |||
== Notes == | == Notes == | ||
<references /> | <references /> | ||
Latest revision as of 07:27, 24 May 2023
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\alt{\mid} \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 . \bot \pipe \in x . t }[/math]
Using the defined rewriting relation, this can be rewritten as follows.
[math]\displaystyle{ \out s . \bot \pipe \in x . t \rew \bot \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. [1] 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 \top) }[/math]
Notes
- ↑ The arrow syntax is unambiguous because variables can always be distinguished from atoms and an atom without polarity does not occur anywhere else in the syntax.