Почему оператор конкатенации @ или арифметические c не являются допустимыми конструкторами шаблонов?

Question

В книге Уллмана по SML

Существуют и другие шаблоны, которые имеют смысл, но недопустимы в ML. Например, мы можем ожидать, что сможем создавать шаблоны, используя оператор конкатенации @ или операторы arithmeti c.

Пример 3.20: Можно ожидать, что мы сможем разбить список на последний элемент и остальную часть списка. Например, мы можем попытаться вычислить длину списка по

fun length(nil) = 0
| length(xs@[x]) = 1 + length(xs);
Error: non-constructor applied to argument in pattern: @
Error: unbound variable or constructor: xs

. Однако, как мы видим, шаблон xs@ [x] недопустим и вызывает два сообщения об ошибках. Первое сообщение жалуется, что @ не является допустимым конструктором шаблона.

Между прочим, мы получаем аналогичную пару сообщений об ошибках, если пытаемся использовать оператор арифметики c для построения шаблона. Например,

fun square(0) = 0
| square(x+l) = 1 + 2*x + square(x);

одинаково ошибочен, даже если он основан на правильном индуктивном определении x ^ 2.

Является ли тот факт, что оператор конкатенации @ или арифметика c операторы не являются законными конструкторами шаблонов, а намеренным дизайном? Почему это так?

Так ли это в большинстве других языков с сопоставлением с образцом?

Спасибо.

Answer 1

Сопоставление с образцом может проверять только структуру значений , оно не может обратить вспять произвольные выражения. 5 является значением. Но 3 + 2 это не так, это выражение, которое создает значение.

Аналогично, C(x, y) - это значение для любого C, который является конструктором типа данных, и любого x, y которые сами являются ценностями. Списки являются просто примером этого случая: :: является конструктором типа данных, тип списка предопределен как

datatype 'a list = nil | :: of 'a * 'a list

(а запись [x,y,z] является просто сокращением для x :: y :: z :: nil.)

Опять же, x @ y отличается, потому что @ - это функция, которая выполняет вычисления, а не конструктор. Сопоставление с образцом не может запускать функции в обратном направлении.

Концептуально значения образуют деревья, например, 5 :: nil - это дерево, root - конструктор :: и два листа которого 5 и * 1028. *. Сопоставление с образцом описывает только возможные разрушения этих деревьев, а не вычисления на деревьях. В результате каждый шаблон является однозначным и соответствует производительности линейно по размеру шаблона.

И да, это относится ко всем языкам.

Answer 2

Да, это намеренно.

@ допускает неоднозначные модели. Если вы разрешили это как образец, что должно означать следующее? Где вы разделяете список ввода?

fun foo (a @ b) =
  Int.max (List.length a, List.length b)

val x = foo [1,2,3,4,5]  (* ??? *)

Есть похожая проблема для +. Функция, которая принимает целое число в качестве аргумента и определяется по шаблонам x+y, может выбрать любые два значения x и y, которые суммируются с аргументом, поэтому значение шаблона является неоднозначным. Это еще более усложняется проблемами переполнения ... например, если у вас была функция fun f (x+1) = ..., а затем вы указали минимальное целое число в качестве аргумента f, что должно произойти?