Mercurial > urweb

comparison doc/manual.tex @ 654:a0f2b070af01

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Revise manual, through end of Syntax
author Adam Chlipala <adamc@hcoop.net>
date Thu, 12 Mar 2009 10:38:13 -0400
parents 9db6880184d0
children 42ca2ab55f91
comparison
equal deleted inserted replaced
653:e5894f0e541a 654:a0f2b070af01
246 &&& \mt{val} \; x : \tau & \textrm{value} \\ 246 &&& \mt{val} \; x : \tau & \textrm{value} \\
247 &&& \mt{structure} \; X : S & \textrm{sub-module} \\ 247 &&& \mt{structure} \; X : S & \textrm{sub-module} \\
248 &&& \mt{signature} \; X = S & \textrm{sub-signature} \\ 248 &&& \mt{signature} \; X = S & \textrm{sub-signature} \\
249 &&& \mt{include} \; S & \textrm{signature inclusion} \\ 249 &&& \mt{include} \; S & \textrm{signature inclusion} \\
250 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\ 250 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
251 &&& \mt{class} \; x & \textrm{abstract type class} \\ 251 &&& \mt{class} \; x :: \kappa & \textrm{abstract constructor class} \\
252 &&& \mt{class} \; x = c & \textrm{concrete type class} \\ 252 &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\
253 \\ 253 \\
254 \textrm{Datatype constructors} & dc &::=& X & \textrm{nullary constructor} \\ 254 \textrm{Datatype constructors} & dc &::=& X & \textrm{nullary constructor} \\
255 &&& X \; \mt{of} \; \tau & \textrm{unary constructor} \\ 255 &&& X \; \mt{of} \; \tau & \textrm{unary constructor} \\
256 \end{array}$$ 256 \end{array}$$
257 257
291 \\ 291 \\
292 &&& \mt{let} \; ed^* \; \mt{in} \; e \; \mt{end} & \textrm{local definitions} \\ 292 &&& \mt{let} \; ed^* \; \mt{in} \; e \; \mt{end} & \textrm{local definitions} \\
293 \\ 293 \\
294 &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e|)^+ & \textrm{pattern matching} \\ 294 &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e|)^+ & \textrm{pattern matching} \\
295 \\ 295 \\
296 &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression} \\ 296 &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression abstraction} \\
297 &&& e \; ! & \textrm{guarded expression application} \\
297 \\ 298 \\
298 &&& \_ & \textrm{wildcard} \\ 299 &&& \_ & \textrm{wildcard} \\
299 &&& (e) & \textrm{explicit precedence} \\ 300 &&& (e) & \textrm{explicit precedence} \\
300 \\ 301 \\
301 \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\ 302 \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\
315 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\ 316 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
316 &&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\ 317 &&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\
317 &&& \mt{table} \; x : c & \textrm{SQL table} \\ 318 &&& \mt{table} \; x : c & \textrm{SQL table} \\
318 &&& \mt{sequence} \; x & \textrm{SQL sequence} \\ 319 &&& \mt{sequence} \; x & \textrm{SQL sequence} \\
319 &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\ 320 &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\
320 &&& \mt{class} \; x = c & \textrm{concrete type class} \\ 321 &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\
321 \\ 322 \\
322 \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \textrm{constant} \\ 323 \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \textrm{constant} \\
323 &&& X & \textrm{variable} \\ 324 &&& X & \textrm{variable} \\
324 &&& M.X & \textrm{projection} \\ 325 &&& M.X & \textrm{projection} \\
325 &&& M(M) & \textrm{functor application} \\ 326 &&& M(M) & \textrm{functor application} \\
338 339
339 The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$. 340 The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$.
340 341
341 A tuple type $(\tau_1, \ldots, \tau_n)$ expands to a record type $\{1 = \tau_1, \ldots, n = \tau_n\}$, with natural numbers as field names. 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. 342 A tuple type $(\tau_1, \ldots, \tau_n)$ expands to a record type $\{1 = \tau_1, \ldots, n = \tau_n\}$, with natural numbers as field names. 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.
342 343
343 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 [c \sim c]$ and allow composite abstractions of the form $\lambda b^+ \Rightarrow c$, elaborating into the obvious sequence of one core $\lambda$ per element of $b^+$. 344 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^+$.
344 345
345 For any signature item or declaration that defines some entity to be equal to $A$ with classification annotation $B$ (e.g., $\mt{val} \; x : B = A$), $B$ and the preceding colon (or similar punctuation) may be omitted, in which case it is filled in as a wildcard. 346 For any signature item or declaration that defines some entity to be equal to $A$ with classification annotation $B$ (e.g., $\mt{val} \; x : B = A$), $B$ and the preceding colon (or similar punctuation) may be omitted, in which case it is filled in as a wildcard.
346 347
347 A signature item or declaration $\mt{type} \; x$ or $\mt{type} \; x = \tau$ is elaborated into $\mt{con} \; x :: \mt{Type}$ or $\mt{con} \; x :: \mt{Type} = \tau$, respectively. 348 A signature item or declaration $\mt{type} \; x$ or $\mt{type} \; x = \tau$ is elaborated into $\mt{con} \; x :: \mt{Type}$ or $\mt{con} \; x :: \mt{Type} = \tau$, respectively.
348 349
349 A signature item or declaration $\mt{class} \; x = \lambda y :: \mt{Type} \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$. 350 A signature item or declaration $\mt{class} \; x = \lambda y \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$.
350 351
351 Handling of implicit and explicit constructor arguments may be tweaked with some prefixes to variable references. An expression $@x$ is a version of $x$ where all implicit constructor arguments have been made explicit. An expression $@@x$ achieves the same effect, additionally halting automatic resolution of type class instances. The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors). 352 Handling of implicit and explicit constructor arguments may be tweaked with some prefixes to variable references. An expression $@x$ is a version of $x$ where all implicit constructor arguments have been made explicit. An expression $@@x$ achieves the same effect, additionally halting automatic resolution of type class instances and automatic proving of disjointness constraints. The default is that any prefix of a variable's type consisting only of implicit polymorphism, type class instances, and disjointness obligations is resolved automatically, with the variable treated as having the type that starts after the last implicit element, with suitable unification variables substituted. The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors).
352 353
353 At the expression level, an analogue is available of the composite $\lambda$ form for constructors. We define the language of binders as $b ::= x \mid (x : \tau) \mid (x \; ? \; \kappa) \mid [c \sim c]$. A lone variable $x$ as a binder stands for an expression variable of unspecified type. 354 At the expression level, an analogue is available of the composite $\lambda$ form for constructors. We define the language of binders as $b ::= x \mid (x : \tau) \mid (x \; ? \; \kappa) \mid X \mid [c \sim c]$. A lone variable $x$ as a binder stands for an expression variable of unspecified type.
354 355
355 A $\mt{val}$ or $\mt{val} \; \mt{rec}$ declaration may include expression binders before the equal sign, following the binder grammar from the last paragraph. Such declarations are elaborated into versions that add additional $\lambda$s to the fronts of the righthand sides, as appropriate. The keyword $\mt{fun}$ is a synonym for $\mt{val} \; \mt{rec}$. 356 A $\mt{val}$ or $\mt{val} \; \mt{rec}$ declaration may include expression binders before the equal sign, following the binder grammar from the last paragraph. Such declarations are elaborated into versions that add additional $\lambda$s to the fronts of the righthand sides, as appropriate. The keyword $\mt{fun}$ is a synonym for $\mt{val} \; \mt{rec}$.
356 357
357 A signature item $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2$. A declaration $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2 = M$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2 = \mt{functor}(X_2 : S_1) : S_2 = M$. 358 A signature item $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2$. A declaration $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2 = M$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2 = \mt{functor}(X_2 : S_1) : S_2 = M$.
358 359