Mercurial > urweb
comparison doc/manual.tex @ 1482:8314f1a309e7
Clarify about implicit folder arguments
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 28 Jun 2011 08:07:20 -0400 |
| parents | a10d080123ec |
| children | a77fa7e7bb7b |
comparison
equal
deleted
inserted
replaced
| 1481:3061d1bf4b2d | 1482:8314f1a309e7 |
|---|---|
| 526 | 526 |
| 527 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. | 527 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. |
| 528 | 528 |
| 529 A signature item or declaration $\mt{class} \; x = \lambda y \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$. | 529 A signature item or declaration $\mt{class} \; x = \lambda y \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$. |
| 530 | 530 |
| 531 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 type class instance and disjointness arguments have been made explicit. An expression $@@x$ achieves the same effect, additionally making explicit all implicit constructor arguments. The default is that implicit arguments are inserted automatically after any reference to a variable, or after any application of a variable to one or more arguments. For such an expression, implicit wildcard arguments are added for the longest prefix of the expression's type consisting only of implicit polymorphism, type class instances, and disjointness obligations. The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors). | 531 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 type class instance and disjointness arguments have been made explicit. (For the purposes of this paragraph, the type family $\mt{Top.folder}$ is a type class, though it isn't marked as one by the usual means.) An expression $@@x$ achieves the same effect, additionally making explicit all implicit constructor arguments. The default is that implicit arguments are inserted automatically after any reference to a variable, or after any application of a variable to one or more arguments. For such an expression, implicit wildcard arguments are added for the longest prefix of the expression's type consisting only of implicit polymorphism, type class instances, and disjointness obligations. The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors). |
| 532 | 532 |
| 533 At the expression level, an analogue is available of the composite $\lambda$ form for constructors. We define the language of binders as $b ::= p \mid [x] \mid [x \; ? \; \kappa] \mid X \mid [c \sim c]$. A lone variable $[x]$ stands for an implicit constructor variable of unspecified kind. The standard value-level function binder is recovered as the type-annotated pattern form $x : \tau$. It is a compile-time error to include a pattern $p$ that does not match every value of the appropriate type. | 533 At the expression level, an analogue is available of the composite $\lambda$ form for constructors. We define the language of binders as $b ::= p \mid [x] \mid [x \; ? \; \kappa] \mid X \mid [c \sim c]$. A lone variable $[x]$ stands for an implicit constructor variable of unspecified kind. The standard value-level function binder is recovered as the type-annotated pattern form $x : \tau$. It is a compile-time error to include a pattern $p$ that does not match every value of the appropriate type. |
| 534 | 534 |
| 535 A local $\mt{val}$ declaration may bind a pattern instead of just a plain variable. As for function arguments, only irrefutable patterns are legal. | 535 A local $\mt{val}$ declaration may bind a pattern instead of just a plain variable. As for function arguments, only irrefutable patterns are legal. |
| 536 | 536 |