Mercurial > urweb

comparison doc/manual.tex @ 1687:e0e19776857d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update manual to fix lexical table and clarify sequencing notation
author Adam Chlipala <adam@chlipala.net>
date Sat, 18 Feb 2012 08:14:51 -0500
parents 0930c92a608e
children 8c2e8d41a8f2
comparison
equal deleted inserted replaced
1686:0930c92a608e 1687:e0e19776857d
346 346
347 \begin{center} 347 \begin{center}
348 \begin{tabular}{rl} 348 \begin{tabular}{rl}
349 \textbf{\LaTeX} & \textbf{ASCII} \\ 349 \textbf{\LaTeX} & \textbf{ASCII} \\
350 $\to$ & \cd{->} \\ 350 $\to$ & \cd{->} \\
351 $\longrightarrow$ & \cd{-->} \\ 351 $\longrightarrow$ & \cd{-{}->} \\
352 $\times$ & \cd{*} \\ 352 $\times$ & \cd{*} \\
353 $\lambda$ & \cd{fn} \\ 353 $\lambda$ & \cd{fn} \\
354 $\Rightarrow$ & \cd{=>} \\ 354 $\Rightarrow$ & \cd{=>} \\
355 $\Longrightarrow$ & \cd{==>} \\ 355 $\Longrightarrow$ & \cd{==>} \\
356 $\neq$ & \cd{<>} \\ 356 $\neq$ & \cd{<>} \\
545 A record type may be written $\{(c = c,)^*\}$, which elaborates to $\$[(c = c,)^*]$. 545 A record type may be written $\{(c = c,)^*\}$, which elaborates to $\$[(c = c,)^*]$.
546 546
547 The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$. 547 The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$.
548 548
549 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. 549 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.
550
551 The syntax $()$ expands to $\{\}$ as a pattern or expression.
550 552
551 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^+$. 553 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^+$.
552 554
553 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 $=$. 555 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 $=$.
554 556
1391 \hspace{.1in} \to \{\mt{Return} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{m} \; \mt{t}, \\ 1393 \hspace{.1in} \to \{\mt{Return} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{m} \; \mt{t}, \\
1392 \hspace{.3in} \mt{Bind} : \mt{t1} ::: \mt{Type} \to \mt{t2} ::: \mt{Type} \to \mt{m} \; \mt{t1} \to (\mt{t1} \to \mt{m} \; \mt{t2}) \to \mt{m} \; \mt{t2}\} \\ 1394 \hspace{.3in} \mt{Bind} : \mt{t1} ::: \mt{Type} \to \mt{t2} ::: \mt{Type} \to \mt{m} \; \mt{t1} \to (\mt{t1} \to \mt{m} \; \mt{t2}) \to \mt{m} \; \mt{t2}\} \\
1393 \hspace{.1in} \to \mt{monad} \; \mt{m} 1395 \hspace{.1in} \to \mt{monad} \; \mt{m}
1394 \end{array}$$ 1396 \end{array}$$
1395 1397
1396 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)$. 1398 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$.
1397 1399
1398 \subsection{Transactions} 1400 \subsection{Transactions}
1399 1401
1400 Ur is a pure language; we use Haskell's trick to support controlled side effects. The standard library defines a monad $\mt{transaction}$, meant to stand for actions that may be undone cleanly. By design, no other kinds of actions are supported. 1402 Ur is a pure language; we use Haskell's trick to support controlled side effects. The standard library defines a monad $\mt{transaction}$, meant to stand for actions that may be undone cleanly. By design, no other kinds of actions are supported.
1401 $$\begin{array}{l} 1403 $$\begin{array}{l}