Как определяется полиморфное сравнение на ADT?

Question

Полиморфная функция compare может использоваться для создания экземпляров предопределенных функторов OCaml (Map.Make, Set.Make, ...).В этом случае нам нужно только знать, что он ведет себя как порядок, но было бы полезно понять, как он на самом деле определен.Например, как убедиться, что следующая функция правильно вычисляет максимум списка:

let rec max_list = function
| [] -> None
| h::t -> max (Some h) (max_list t)

Сначала я подумал, что конструкторы, определенные ранее, меньше, чем конструкторы, определенные позже.Однако, похоже, это не так, поскольку max Non (Som 2) имеет значение Som 2 : opt, определено ли opt как type 'a opt = Non | Some of 'a или как type 'a opt = Some of 'a | Non.

Чтобы сравнить значения алгебраического типа данных, яожидать, что он сравнивает конструкторы, а затем, если они совпадают, сравнивает их аргументы.Почему это не так, и как определяется сравнение?

Answer 1

Если вы посмотрите на определение языка для функции compare и предыдущих операторов сравнения (в настоящее время https://caml.inria.fr/pub/docs/manual-ocaml-4.08/core.html#sec551), вы увидите, что нет явной гарантии порядка различных конструкторов типа варианта).Только гарантируется, что он представляет общий порядок.

Если вы хотите конкретный порядок, вам нужно определить собственную функцию сравнения.

В текущей реализации конструкторы без аргументов (нулевые конструкторы) обрабатываются как меньшие, чем конструкторы с аргументами, даже если они появляются позже в определении. На мой взгляд, было бы неразумно полагаться на это, поскольку в определении языка нет явной гарантии.

# type ab = B of int | A;;
type ab = B of int | A
# A < B 2;;
- : bool = true
# type cd = C | D of int;;
type cd = C | D of int
# C < D 2;;
- : bool = true
# type ef = E | F;;
type ef = E | F
# E < F;;
- : bool = true