Shorthands

There are a variety of derived syntactic forms that elaborate into the core syntax from the last subsection. We will present the additional forms roughly following the order in which we presented the constructs that they elaborate into.

In many contexts where record fields are expected, like in a projection $e.c$ , a constant field may be written as simply $X$ , rather than $\char93 X$ .

A record type may be written $\{(c = c,)^*\}$ , which elaborates to $\$[(c = c,)^*]$ .

The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$ .

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.

The syntax $()$ expands to $\{\}$ as a pattern or expression.

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^+$ .

Further, the signature item or declaration syntax $\mathsf{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 $=$ .

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.

For any signature item or declaration that defines some entity to be equal to $A$ with classification annotation $B$ (e.g., $\mathsf{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.

A signature item or declaration $\mathsf{type} \; x$ or $\mathsf{type} \; x = \tau$ is elaborated into $\mathsf{con} \; x :: \mathsf{Type}$ or $\mathsf{con} \; x :: \mathsf{Type} = \tau$ , respectively.

A signature item or declaration $\mathsf{class} \; x = \lambda y \Rightarrow c$ may be abbreviated $\mathsf{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 type class instance and disjointness arguments have been made explicit. (For the purposes of this paragraph, the type family $\mathsf{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.

A local $\mathsf{val}$ declaration may bind a pattern instead of just a plain variable. As for function arguments, only irrefutable patterns are legal.

The keyword $\mathsf{fun}$ is a shorthand for $\mathsf{val} \; \mathsf{rec}$ that allows arguments to be specified before the equal sign in the definition of each mutually recursive function, as in SML. Each curried argument must follow the grammar of the $b$ non-terminal introduced two paragraphs ago. A $\mathsf{fun}$ declaration is elaborated into a version that adds additional $\lambda$ s to the fronts of the righthand sides, as appropriate.

A signature item $\mathsf{functor} \; X_1 \; (X_2 : S_1) : S_2$ is elaborated into $\mathsf{structure} \; X_1 : \mathsf{functor}(X_2 : S_1) : S_2$ . A declaration $\mathsf{functor} \; X_1 \; (X_2 : S_1) : S_2 = M$ is elaborated into $\mathsf{structure} \; X_1 : \mathsf{functor}(X_2 : S_1) : S_2 = \mathsf{functor}(X_2 : S_1) : S_2 = M$ .

An $\mathsf{open} \; \mathsf{constraints}$ declaration is implicitly inserted for the argument of every functor at the beginning of the functor body. For every declaration of the form $\mathsf{structure} \; X : S = \mathsf{struct} \ldots \mathsf{end}$ , an $\mathsf{open} \; \mathsf{constraints} \; X$ declaration is implicitly inserted immediately afterward.

A declaration $\mathsf{table} \; x : \{(c = c,)^*\}$ is elaborated into $\mathsf{table} \; x : [(c = c,)^*]$ .

The syntax $\mathsf{where} \; \mathsf{type}$ is an alternate form of $\mathsf{where} \; \mathsf{con}$ .

The syntax $\mathsf{if} \; e \; \mathsf{then} \; e_1 \; \mathsf{else} \; e_2$ expands to $\mathsf{case} \; e \; \mathsf{of} \; \mathsf{Basis}.\mathsf{True} \Rightarrow e_1 \mid \mathsf{Basis}.\mathsf{False} \Rightarrow e_2$ .

There are infix operator syntaxes for a number of functions defined in the $\mathsf{Basis}$ module. There is $=$ for $\mathsf{eq}$ , $\neq$ for $\mathsf{neq}$ , $-$ for $\mathsf{neg}$ (as a prefix operator) and $\mathsf{minus}$ , $+$ for $\mathsf{plus}$ , $\times$ for $\mathsf{times}$ , $/$ for $\mathsf{div}$ , $\%$ for $\mathsf{mod}$ , $<$ for $\mathsf{lt}$ , $\leq$ for $\mathsf{le}$ , $>$ for $\mathsf{gt}$ , and $\geq$ for $\mathsf{ge}$ .

A signature item $\mathsf{table} \; x : c$ is shorthand for $\mathsf{val} \; x : \mathsf{Basis}.\mathsf{sql\_table} \; c \; []$ . $\mathsf{view} \; x : c$ is shorthand for $\mathsf{val} \; x : \mathsf{Basis}.\mathsf{sql\_view} \; c$ , $\mathsf{sequence} \; x$ is short for $\mathsf{val} \; x : \mathsf{Basis}.\mathsf{sql\_sequence}$ . $\mathsf{cookie} \; x : \tau$ is shorthand for $\mathsf{val} \; x : \mathsf{Basis}.\mathsf{http\_cookie} \; \tau$ , and $\mathsf{style} \; x$ is shorthand for $\mathsf{val} \; x : \mathsf{Basis}.\mathsf{css\_class}$ .

It is possible to write a $\mathsf{let}$ expression with its constituents in reverse order, along the lines of Haskell's where. An expression $\mathsf{let} \; e \; \mathsf{where} \; ed^* \; \mathsf{end}$ desugars to $\mathsf{let} \; ed^* \; \mathsf{in} \; e \; \mathsf{end}$ .