Когда нужны случаи опровержения в OCaml?

В разделе GADT главы "aa Расширения языка" официальных документов OCaml представлены случаи опровержения формы _ -> .. Тем не менее, я думал, что сопоставление с образцом уже было исчерпывающим, поэтому я не уверен, когда фактически требуется опровержение.

Пример, приведенный в документе, выглядит следующим образом:

type _ t =
  | Int : int t
  | Bool : bool t

let deep : (char t * int) option -> char = function
  | None -> 'c'
  | _ -> .

Но даже в документах говорится, что этот случай опровержения является излишним. Есть ли пример, когда для проверки типа необходим случай опровержения?

Ответ 1

Случаи опровержения полезны для полной проверки, а не для прямой проверки типов.

Ваш пример немного сбивает с толку, потому что компилятор автоматически добавляет простой случай опровержения | _ -> ., когда сопоставление с образцом достаточно простое. другими словами,

let deep : (char t * int) option -> char = function None -> 'c'

эквивалентно

let deep : (char t * int) option -> char = function
  | None -> 'c'
  | _ -> .

потому что проверщик типов сам добавляет опровержение. До введения случаев опровержения в 4.03 единственный способ написать deep был

let deep : (char t * int) option -> char = function
  | None -> 'c'

Предупреждение 8: это сопоставление с образцом не является исчерпывающим. Вот пример значения, которое не соответствует:
Некоторые _

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

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

let either : (float t, char t) result -> char = ...

нет способа завершить многоточие ..., используя конкретные образцы с правильными типами:

let either : (float t, char t) result -> char = function
  | Ok Int -> ... (* no, wrong type: (int t, _ ) result *)
  | Ok Bool -> ... (* still no possible (bool t, _) result *)
  | Error Int -> ... (* not working either: (_, int t) result *)
  | Error Bool -> ... (* yep, impossible (_, bool t) result *)

Случаи опровержения - это способ указать проверщику типов, что оставшиеся случаи шаблона не совместимы с существующими ограничениями типов

let either : (float t, char t) result -> char = function
  | Ok _ -> .
  | _ -> .

Точнее, эти случаи опровержения говорят компилятору о том, чтобы попытаться развернуть все шаблоны _ в левой части случая и проверить, что у этих шаблонов нет возможности проверить тип.

В целом, существует три типа ситуаций, когда требуется рукописное опровержение:

Сопоставление с образцом для типа без каких-либо возможных значений
Случай автоматического опровержения не был добавлен
Глубина исследования контрпримеров по умолчанию недостаточна

Во-первых, самый простой пример с игрушкой происходит, когда нет возможных шаблонов:

let f : float t -> _ = function _ -> .

Второй случай, когда кто-то выпадает из случая опровержения по умолчанию. В частности, случай опровержения добавляется только тогда, когда в match есть один случай:

type 'a ternary = A | B | C of 'a
let ternary : float t ternary -> _ = function
  | A -> ()
  | B -> ()

Предупреждение 8: это сопоставление с образцом не является исчерпывающим. Вот пример случая, который не соответствует: C _

Таким образом, рукописный случай необходим

let ternary : float t ternary -> _ = function
  | A -> ()
  | B -> ()
  | _ -> .

Наконец, иногда глубины исследования по умолчанию для контрпримеров недостаточно, чтобы доказать, что контрпримеров нет. По умолчанию глубина исследования равна 1: шаблон _ взорван один раз. Например, в вашем примере | _ -> . преобразуется в Int | Bool -> ., затем средство проверки типов проверяет, что никакие случаи не являются действительными.

Следовательно, простой способ сделать опровержение необходимым - это вложить два типа конструкторов. Например:

let either : (float t, char t) result -> char = function
  | _ -> .

Ошибка: этот случай совпадения не может быть опровергнут. Вот пример значения, которое достигнет его: _

Здесь необходимо расширить вручную хотя бы один из случаев Ok или Error:

let either : (float t, char t) result -> char = function
  | Ok _ -> .
  | _ -> .

Обратите внимание, что существует особый случай для типов с одним конструктором, который при раскрытии учитывает только 1/5 полного раскрытия. Например, если вы введете тип

type 'a delay = A of 'a

затем

let nested : float t delay option -> _ = function
  | None -> ()

хорошо, потому что расширение _ до A _ стоит 0,2, а у нас все еще есть некоторый бюджет для расширения A _ до A Int | A Float.

Тем не менее, если вы вложите достаточно delay s, появится предупреждение

let nested : float t delay delay delay delay delay delay option -> _ = function
  | None -> ()

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

Предупреждение может быть исправлено путем добавления опровержения:

let nested : float t delay delay delay delay delay delay option -> _ = function
  | None -> ()
  | Some A _ -> .