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 , a constant field may be written as simply , rather than .
A record type may be written , which elaborates to .
The notation is shorthand for .
A tuple type expands to a record type , with natural numbers as field names. A tuple expression expands to a record expression . A tuple pattern expands to a rigid record pattern . 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 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 and allow composite abstractions of the form , elaborating into the obvious sequence of one core per element of .
Further, the signature item or declaration syntax is shorthand for wrapping of the appropriate s around the righthand side . The elements may not include , and there may also be an optional before the .
In some contexts, the parser isn't happy with token sequences like , to indicate a constructor variable of wildcard kind. In such cases, write the second two tokens as , with no intervening spaces. Analogous syntax is available for implicit constructor arguments.
For any signature item or declaration that defines some entity to be equal to with classification annotation (e.g., ), 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 or is elaborated into or , respectively.
A signature item or declaration may be abbreviated .
Handling of implicit and explicit constructor arguments may be tweaked with some prefixes to variable references. An expression is a version of where all type class instance and disjointness arguments have been made explicit. (For the purposes of this paragraph, the type family 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 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 form for constructors. We define the language of binders as . A lone variable stands for an implicit constructor variable of unspecified kind. The standard value-level function binder is recovered as the type-annotated pattern form . It is a compile-time error to include a pattern that does not match every value of the appropriate type.
A local declaration may bind a pattern instead of just a plain variable. As for function arguments, only irrefutable patterns are legal.
The keyword is a shorthand for 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 non-terminal introduced two paragraphs ago. A declaration is elaborated into a version that adds additional s to the fronts of the righthand sides, as appropriate.
A signature item is elaborated into . A declaration is elaborated into .
An declaration is implicitly inserted for the argument of every functor at the beginning of the functor body. For every declaration of the form , an declaration is implicitly inserted immediately afterward.
A declaration is elaborated into .
The syntax is an alternate form of .
The syntax expands to .
There are infix operator syntaxes for a number of functions defined in the module. There is for , for , for (as a prefix operator) and , for , for , for , for , for , for , for , and for .
A signature item is shorthand for . is shorthand for , is short for . is shorthand for , and is shorthand for .
It is possible to write a expression with its constituents in reverse order, along the lines of Haskell's where. An expression desugars to .