summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-12-30 09:48:32 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-12-30 09:48:32 -0500
commitb52a0b1b4485024429c3f51bf8a9e82ec5ebe2ca (patch)
tree976497a7606247ab0c62a86e1572721ff08cc105
parent9c5df80840ed4fc429f1727480ddec78c4cc2204 (diff)
Update manual's description of implicit arguments
-rw-r--r--doc/manual.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 07f96398..1f7a774b 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -465,7 +465,7 @@ A signature item or declaration $\mt{type} \; x$ or $\mt{type} \; x = \tau$ is e
A signature item or declaration $\mt{class} \; x = \lambda y \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$.
-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).
+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 implicit arguments are inserted automatically after any reference to a non-local variable, or after any application of a non-local 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).
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.