MLton

Standard ML has special syntax for products (tuples). A product type is written as

t1 * t2 * ... * tN

and a product pattern is written as

(p1, p2, ..., pN)

In most situations the syntax is quite convenient. However, there are situations where the syntax is cumbersome. There are also situations in which it is useful to construct and destruct n-ary products inductively, especially when using Fold.

In such situations, it is useful to have a binary product datatype with an infix constructor defined as follows.

datatype ('a, 'b) product = & of 'a * 'b
infix &

With these definitions, one can write an n-ary product as a nested binary product quite conveniently.

x1 & x2 & ... & xn

Because of left associativity, this is the same as

(((x1 & x2) & ...) & xn)

Because & is a constructor, the syntax can also be used for patterns.

The symbol & is inspired by the Curry-Howard isomorphism: the proof of a conjunction (A & B) is a pair of proofs (a, b).

Example: parser combinators

A typical parser combinator library provides a combinator that has a type of the form.

'a parser * 'b parser -> ('a * 'b) parser

and produces a parser for the concatenation of two parsers. When more than two parsers are concatenated, the result of the resulting parser is a nested structure of pairs

(...((p1, p2), p3)..., pN)

which is somewhat cumbersome.

By using a product type, the type of the concatenation combinator then becomes

'a parser * 'b parser -> ('a, 'b) product parser

While this doesn’t stop the nesting, it makes the pattern significantly easier to write. Instead of

(...((p1, p2), p3)..., pN)

the pattern is written as

p1 & p2 & p3 & ... & pN

which is considerably more concise.

Also see