### changeset 1687:e0e19776857d

Update manual to fix lexical table and clarify sequencing notation
author Adam Chlipala Sat, 18 Feb 2012 08:14:51 -0500 0930c92a608e 8c2e8d41a8f2 doc/manual.tex 1 files changed, 4 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/doc/manual.tex	Sat Feb 04 11:08:56 2012 -0500
+++ b/doc/manual.tex	Sat Feb 18 08:14:51 2012 -0500
@@ -348,7 +348,7 @@
\begin{tabular}{rl}
\textbf{\LaTeX} & \textbf{ASCII} \\
$\to$ & \cd{->} \\
-    $\longrightarrow$ & \cd{-->} \\
+    $\longrightarrow$ & \cd{-{}->} \\
$\times$ & \cd{*} \\
$\lambda$ & \cd{fn} \\
$\Rightarrow$ & \cd{=>} \\
@@ -548,6 +548,8 @@

A tuple type $\tau_1 \times \ldots \times \tau_n$ expands to a record type $\{1 : \tau_1, \ldots, n : \tau_n\}$, with natural numbers as field names.  A tuple expression $(e_1, \ldots, e_n)$ expands to a record expression $\{1 = e_1, \ldots, n = e_n\}$.  A tuple pattern $(p_1, \ldots, p_n)$ expands to a rigid record pattern $\{1 = p_1, \ldots, n = p_n\}$.  Positive natural numbers may be used in most places where field names would be allowed.

+The syntax $()$ expands to $\{\}$ as a pattern or expression.
+
In general, several adjacent $\lambda$ forms may be combined into one, and kind and type annotations may be omitted, in which case they are implicitly included as wildcards.  More formally, for constructor-level abstractions, we can define a new non-terminal $b ::= x \mid (x :: \kappa) \mid X$ and allow composite abstractions of the form $\lambda b^+ \Rightarrow c$, elaborating into the obvious sequence of one core $\lambda$ per element of $b^+$.

Further, the signature item or declaration syntax $\mt{con} \; x \; b^+ = c$ is shorthand for wrapping of the appropriate $\lambda$s around the righthand side $c$.  The $b$ elements may not include $X$, and there may also be an optional $:: \kappa$ before the $=$.
@@ -1393,7 +1395,7 @@
\end{array}
-The Ur/Web compiler provides syntactic sugar for monads, similar to Haskell's \cd{do} notation.  An expression $x \leftarrow e_1; e_2$ is desugared to $\mt{bind} \; e_1 \; (\lambda x \Rightarrow e_2)$, and an expression $e_1; e_2$ is desugared to $\mt{bind} \; e_1 \; (\lambda () \Rightarrow e_2)$.
+The Ur/Web compiler provides syntactic sugar for monads, similar to Haskell's \cd{do} notation.  An expression $x \leftarrow e_1; e_2$ is desugared to $\mt{bind} \; e_1 \; (\lambda x \Rightarrow e_2)$, and an expression $e_1; e_2$ is desugared to $\mt{bind} \; e_1 \; (\lambda () \Rightarrow e_2)$.  Note a difference from Haskell: as the $e_1; e_2$ case desugaring involves a function with $()$ as its formal argument, the type of $e_1$ must be of the form $m \; \{\}$, rather than some arbitrary $m \; t$.