From 16b6fdce0bab0699fcf16f41991976b386181dd1 Mon Sep 17 00:00:00 2001 From: Matthew Dempsky Date: Wed, 22 Jan 2020 14:43:26 -0800 Subject: Kind variables must be bracketed in expression-level binders --- doc/manual.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/manual.tex b/doc/manual.tex index 44cd0007..fc59deec 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -644,7 +644,7 @@ A signature item or declaration $\mt{class} \; x = \lambda y \Rightarrow c$ may 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; and any record type is considered to be a type class instance type when every field's type is a type class instance type.) 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). -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. +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. A local $\mt{val}$ declaration may bind a pattern instead of just a plain variable. As for function arguments, only irrefutable patterns are legal. -- cgit v1.2.3 From 15359c4e8e4546f789dfd316109aea6aa629e96e Mon Sep 17 00:00:00 2001 From: Matthew Dempsky Date: Wed, 22 Jan 2020 14:26:23 -0800 Subject: Consistently introduce application syntax before abstraction Makes it slightly easier to recognize the symmetry between forms. --- doc/manual.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/manual.tex b/doc/manual.tex index fc59deec..2a3f21d6 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -486,8 +486,8 @@ $$\begin{array}{rrcll} &&& c \; c & \textrm{type-level function application} \\ &&& \lambda x \; :: \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\ \\ - &&& X \Longrightarrow c & \textrm{type-level kind-polymorphic function abstraction} \\ &&& c [\kappa] & \textrm{type-level kind-polymorphic function application} \\ + &&& X \Longrightarrow c & \textrm{type-level kind-polymorphic function abstraction} \\ \\ &&& () & \textrm{type-level unit} \\ &&& \#X & \textrm{field name} \\ @@ -574,8 +574,8 @@ $$\begin{array}{rrcll} \\ &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e|)^+ & \textrm{pattern matching} \\ \\ - &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression abstraction} \\ &&& e \; ! & \textrm{guarded expression application} \\ + &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression abstraction} \\ \\ &&& \_ & \textrm{wildcard} \\ &&& (e) & \textrm{explicit precedence} \\ -- cgit v1.2.3 From 3256b037dafdb0818589ca475df5e2aed64f1af2 Mon Sep 17 00:00:00 2001 From: Matthew Dempsky Date: Wed, 22 Jan 2020 15:23:04 -0800 Subject: Elaborate e^* and e^+ syntax Clarify that parentheses are used if and only if e consists of multiple symbols; also, that both e and the separator (if any) will be paranthesized. ("if any" is appropriate because the grammar extensions for XML include "(x[=v])*", which has no separator.) Fix the known-length type-level record syntax to indicate that commas are used to separate field descriptors. Change the pattern matching grammar to use "\mid" instead of "|" for internal consistency. (No visible change, as far as I can tell.) --- doc/manual.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/manual.tex b/doc/manual.tex index 2a3f21d6..b6febfaa 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -443,7 +443,7 @@ We give the Ur language definition in \LaTeX $\;$ math mode, since that is prett \end{tabular} \end{center} -We often write syntax like $e^*$ to indicate zero or more copies of $e$, $e^+$ to indicate one or more copies, and $e,^*$ and $e,^+$ to indicate multiple copies separated by commas. Another separator may be used in place of a comma. The $e$ term may be surrounded by parentheses to indicate grouping; those parentheses should not be included in the actual ASCII. +We often write syntax like $e^*$ to indicate zero or more copies of $e$, $e^+$ to indicate one or more copies, and $e,^*$ and $e,^+$ to indicate multiple copies separated by commas. Another separator may be used in place of a comma. When $e$ consists of multiple symbols, the $e$ term and separator (if any) are surrounded by parentheses to indicate grouping; those parentheses should not be included in the actual ASCII. We write $\ell$ for literals of the primitive types, for the most part following C conventions. There are $\mt{int}$, $\mt{float}$, $\mt{char}$, and $\mt{string}$ literals. Character literals follow the SML convention instead of the C convention, written like \texttt{\#"a"} instead of \texttt{'a'}. @@ -492,7 +492,7 @@ $$\begin{array}{rrcll} &&& () & \textrm{type-level unit} \\ &&& \#X & \textrm{field name} \\ \\ - &&& [(c = c)^*] & \textrm{known-length type-level record} \\ + &&& [(c = c,)^*] & \textrm{known-length type-level record} \\ &&& c \rc c & \textrm{type-level record concatenation} \\ &&& \mt{map} & \textrm{type-level record map} \\ \\ @@ -572,7 +572,7 @@ $$\begin{array}{rrcll} \\ &&& \mt{let} \; ed^* \; \mt{in} \; e \; \mt{end} & \textrm{local definitions} \\ \\ - &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e|)^+ & \textrm{pattern matching} \\ + &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e\mid)^+ & \textrm{pattern matching} \\ \\ &&& e \; ! & \textrm{guarded expression application} \\ &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression abstraction} \\ -- cgit v1.2.3