Function and Product Types Peculiarity

Question

What is the difference between the types

(seq of nat * seq of nat) -> nat

and

seq of nat * seq of nat -> nat

According to the Language Reference Manual * has higher precedence than -> so the parentheses have no effect; the are semantically the same. But consider the function definitions

length: (seq of nat * seq of nat) -> nat
length (mk_(l,m)) == len l + len m;

length0: seq of nat * seq of nat -> nat
length0 (l,m) == len l + len m;

Each uses one of the types, and the patterns used in the definitions have to be different to pass type checking. It seems there is a difference between the two types. What is going on here? By parenthesising it interprets the argument as a product, but without the parentheses there are two arguments but somehow the argument type of the function is still a product. It is rather confusing. Can someone clarify?

Answer 1

Yes, this is confusing. In effect, brackets are being used for two purposes here, and it isn't made clear in the grammar. In isolation, brackets can be used in a type declaration to indicate groupings and overcome the default precedence. This is as you would expect. But in a function definition, top level brackets and stars are also to identify separate parameter types.

So "nat * nat -> nat" is trying to indicate that this is a function with two parameters, rather than that this is a function that takes a single argument of a product type. So how can you indicate that you genuinely want a single product argument? Answer: with brackets :-)

So the outermost layer of bracketing and product operators in a function definition are used to group parameters types, but deeper brackets and stars have the usual meaning. The grammar is misleading when it says that the parameters/return type is a "function type" - syntactically this is true, but the way the type is then interpreted is special, in order to pull out the parameter number and types for the function.