Mercurial > urweb
comparison doc/manual.tex @ 1687:e0e19776857d
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} |