4 Product types and arities of functions

Design proposal: Allow unary functions only, but product types. Products can be 0-ary or n-ary for n > 2 (the unary product of a type is just the type itself). Associated to each product type is a tupling constructor function (then selector functions are user-definable). N-ary functions are obtained either by currying or by product types.

This is adopted in many functional languages. Of course, product types are user-definable. But the composition of two functions f: t --> t₁×t₂ and g: t₁×t₂ --> u can be expressed directly only with product types.
Alternatives:

1. Allow n-ary functions, but no product types. This mixes up products with function spaces; we find it more natural to keep both separated.
2. Allow unary functions only, and no product types, see [Far91]. N-ary functions are obtained by currying. This is no extension of first-order CASL.

Arities of predicates should be treated in the same way as arities of functions.