Mercurial > urweb

comparison doc/manual.tex @ 1574:644558d9c756

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Extend and document 'con' syntax with arguments
author Adam Chlipala <adam@chlipala.net>
date Sat, 15 Oct 2011 10:05:13 -0400
parents 34364e383bed
children 7d2aa0ddc531
comparison
equal deleted inserted replaced
1573:34364e383bed 1574:644558d9c756
378 &&& \mt{Name} & \textrm{field names} \\ 378 &&& \mt{Name} & \textrm{field names} \\
379 &&& \kappa \to \kappa & \textrm{type-level functions} \\ 379 &&& \kappa \to \kappa & \textrm{type-level functions} \\
380 &&& \{\kappa\} & \textrm{type-level records} \\ 380 &&& \{\kappa\} & \textrm{type-level records} \\
381 &&& (\kappa\times^+) & \textrm{type-level tuples} \\ 381 &&& (\kappa\times^+) & \textrm{type-level tuples} \\
382 &&& X & \textrm{variable} \\ 382 &&& X & \textrm{variable} \\
383 &&& X \longrightarrow k & \textrm{kind-polymorphic type-level function} \\ 383 &&& X \longrightarrow \kappa & \textrm{kind-polymorphic type-level function} \\
384 &&& \_\_ & \textrm{wildcard} \\ 384 &&& \_\_ & \textrm{wildcard} \\
385 &&& (\kappa) & \textrm{explicit precedence} \\ 385 &&& (\kappa) & \textrm{explicit precedence} \\
386 \end{array}$$ 386 \end{array}$$
387 387
388 Ur supports several different notions of functions that take types as arguments. These arguments can be either implicit, causing them to be inferred at use sites; or explicit, forcing them to be specified manually at use sites. There is a common explicitness annotation convention applied at the definitions of and in the types of such functions. 388 Ur supports several different notions of functions that take types as arguments. These arguments can be either implicit, causing them to be inferred at use sites; or explicit, forcing them to be specified manually at use sites. There is a common explicitness annotation convention applied at the definitions of and in the types of such functions.
546 The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$. 546 The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$.
547 547
548 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. 548 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 549
550 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^+$. 550 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^+$.
551
552 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 $=$.
551 553
552 In some contexts, the parser isn't happy with token sequences like $x :: \_$, to indicate a constructor variable of wildcard kind. In such cases, write the second two tokens as $::\hspace{-.05in}\_$, with no intervening spaces. Analogous syntax $:::\hspace{-.05in}\_$ is available for implicit constructor arguments. 554 In some contexts, the parser isn't happy with token sequences like $x :: \_$, to indicate a constructor variable of wildcard kind. In such cases, write the second two tokens as $::\hspace{-.05in}\_$, with no intervening spaces. Analogous syntax $:::\hspace{-.05in}\_$ is available for implicit constructor arguments.
553 555
554 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. 556 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.
555 557