t1 * t2 * ... * tNand 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 & ... & pNwhich is considerably more concise.