identifier:

ch+

placeholder:

'_'

integer:

digit+

string:

'"' ch* '"'

The characters ch in the string may be anything but double-quote, backslash, or newline.

comment:

'#' ch* newline

expression:

parenthesized-term

bracketed-coterm

• A file represents an I/O action, either strictly as a term or lazily as a coterm.

parenthesized-term:

'(' term ( ':' type )opt ')'

term:

'&' ( secondary '&' )*

',' ( secondary ',' )*

bracketed-coterm

copattern '<+' secondary '$' cosecondary

secondary

• Terms delimited by '&' are tuples.
• Terms delimited by ',' are lists.
• Square brackets within a term form a continuation of the enclosed coterm.
• An abstraction reduces a secondary term with a coterm, delivering a result value via the copattern.

secondary:

'\' pattern '->' secondary

'@' identifier ':>' secondary

primary secondary

primary

• Backslash starts a lambda expression for a function value.
• At-sign introduces the type parameter of a generic term. The scope of the identifier is the secondary. Except where redefined, the identifier may be used only as a type, not as a term or coterm.
• A primary term is passed by value as an argument by juxtaposing it with a function to its right. Neither the argument nor the function may be an empty term.

primary:

identifier

( )

integer

string

'{' binding* secondary '}'

parenthesized-term

• An empty term represents a trivial, or void value.
• Curly braces indicate an I/O action.

binding:

secondary ( '=:' pattern )opt ';'

• A binding processes the secondary term, optionally binding its result to a pattern. Subsequent terms within the same curly braces may refer names defined by the pattern.

pattern:

'&' ( ( primary-pattern | placeholder ) '&' )*

'@' ( type ':>' )opt pattern

primary-pattern

• A tuple pattern can bind multiple identifiers. Sub-patterns may be omitted if no reference to that field is needed.
• At-sign starts a pattern which binds to a generic type, and optionally indicates the specific type at which it is to apply.

primary-pattern:

identifier

( )

'[' copattern ']'

'(' pattern ')'

• An identifier is the fundamental pattern, bound to an argument value as in an ordinary function definition. The scope of the identifier is the body of the lambda or abstraction containing the pattern. Except where redefined, the identifier may be used only as a primary term, not as a coterm or type.
• An empty pattern binds a void value.
• A bracketed copattern binds to a continuation, so that its covalue may be referred to.

bracketed-coterm:

'[' coterm ( ':' type )opt ']'

coterm:

'|' ( cosecondary '|' )*

',' ( cosecondary ',' )*

parenthesized-term

pattern '->' secondary '$' cosecondary

cosecondary

• Coterms delimited by '|' provide a set of covalues that handle the corresponding cases of a matching value.
• Coterms delimited by ',' are colists [whatever that means].
• Parentheses within a coterm denote a use of the enclosed term.
• An abstraction makes available a value via the pattern, and reduces a secondary term with a coterm.

cosecondary:

'\' copattern '<+' cosecondary

'@' identifier '<:' cosecondary

coprimary cosecondary

coprimary

• Backslash starts a lambda for a cofunction covalue.
• At-sign introduces the type parameter representing an abstract type. The scope of the identifier is the cosecondary. Except where redefined, the identifier may be used only as a type, not as a term or coterm.
• A primary coterm is passed by name as an argument by juxtaposing it with a cofunction to its right. Neither the argument nor the function may be an empty coterm.

coprimary:

identifier

( )

integer

string

'{' cobinding* cosecondary '}'

bracketed-coterm

• An empty coterm represents an unreachable covalue.
• An integer or string within a coterm is a covalue suitable for passing by name.
• Curly braces indicate an I/O action.

cobinding:

cosecondary ( '=:' copattern )opt ';'

• A cobinding processes the secondary coterm, optionally binding its result lazily to a copattern. Subsequent coterms within the same curly braces may refer to names defined by the copattern.

copattern:

'|' ( ( primary-copattern | placeholder ) '|' )*

'@' ( type '<:' )opt copattern

primary-copattern

• A case pattern can bind multiple identifiers. Sub-patterns may be omitted if no reference to that case is needed.
• At-sign starts a pattern which packages an abstract type, and optionally indicates the concrete type used by the implementation.

primary-copattern:

identifier

( )

'(' pattern ')'

'[' copattern ']'

• An identifier is the fundamental copattern, bound to an argument covalue as in a simple non-strict function definition. The scope of the identifier is the body of the lambda or abstraction containing the pattern. Except where redefined, the identifier may be used only as a coprimary coterm, not as a term or type.
• An empty copattern binds an unreachable covalue.
• A parenthesized pattern binds to a covalue that uses a value, so that the value may be referred to.

type:

'∀' identifier '.' type

'∃' identifier '.' type

'\' identifier '.' type

quaternary‑type

• '∀' (alternatively 'all') forms a universal type, e.g. the type of a generic function.
• '∃' (alternatively 'some') forms an existential type, e.g. the type of a package that implements an abstract type.
• '\' forms a concrete type constructor.

quaternary‑type:

tertiary‑type '→' quaternary‑type

tertiary‑type '↚' quaternary‑type

tertiary‑type

• '→' or '->' indicates the type of a by-value function term.
• '↚' or '<+' indicates the type of a by-name cofunction coterm.

tertiary‑type:

'¬' tertiary‑type

secondary‑type

• '¬' (alternatively '~') forms a negation type, e.g. the type of a continuation.

secondary‑type:

secondary‑type primary‑type

primary‑type

• When types are juxtaposed, the left must be a type constructor applied to the right type.

primary‑type:

identifier

placeholder

'(' type ')'

'(' '∧' ( type '∧')* ')'

'(' '∨' ( type '∨')* ')'

'(,' type ',)'

'[,' type ',]'

• A type identifier may refer to a builtin type or one defined within the program. It may be an ordinary type or a type constructor.
• A placeholder does not specify or constrain the type. It is inferred.
• '∧' or '&' indicates a logical 'and' or product type. A value of this type is a tuple of 0 or more values.
• '∨' or '|' indicates a logical 'or' (i.e. sum) type. A value of this type designates one of the contained types, for which it provides a value.
• ',' indicates the type of a list of any number of elements with a common type.