Особенности функций и типов продукции

Question

В чем разница между типами

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

а также

seq of nat * seq of nat -> nat

Согласно справочному руководству по языку * имеет более высокий приоритет, чем -> поэтому скобки не имеют никакого эффекта; семантически одинаковы. Но рассмотрим определения функций

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;

Каждый использует один из типов, и шаблоны, используемые в определениях, должны отличаться, чтобы пройти проверку типов. Кажется, есть разница между этими двумя типами. Что здесь происходит? Заключив скобки, он интерпретирует аргумент как продукт, но без скобок есть два аргумента, но каким-то образом тип аргумента функции все еще является продуктом. Это довольно запутанно. Может кто-нибудь уточнить?

Answer 1

Да, это сбивает с толку. Фактически, здесь скобки используются для двух целей, и это не ясно из грамматики. В отдельности скобки могут использоваться в объявлении типа для указания групп и преодоления приоритета по умолчанию. Это то, что вы ожидаете. Но в определении функции скобки верхнего уровня и звезды также должны идентифицировать отдельные типы параметров.

Поэтому "nat * nat -> nat" пытается указать, что это функция с двумя параметрами, а не функция, которая принимает один аргумент типа продукта. Так как же вы можете указать, что вам действительно нужен один аргумент продукта? Ответ: в скобках:-)

Таким образом, внешний слой скобок и операторы произведения в определении функции используются для группировки типов параметров, но более глубокие скобки и звездочки имеют обычное значение. Грамматика вводит в заблуждение, когда говорит, что тип параметров / возврата является "типом функции" - синтаксически это правда, но способ интерпретации типа является специальным, чтобы вытащить номер параметра и типы для функции.