Когда в OCaml необходимы случаи опровержения? - PullRequest
Новая
       60

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

0 голосов
/ 13 октября 2018

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

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

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

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

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

1 Ответ

0 голосов
/ 13 октября 2018

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

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

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 *)
  | Either Bool -> ... (* yep, impossible (_, bool t) result *)

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

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

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

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

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

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

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

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

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

имеется только один случай: это сопоставление с образцом не является исчерпывающим.Вот пример случая, который не соответствует: 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 _ -> .
...