Блог

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

 let {name} [a; b; {...}] =
  {...}
  

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

С другой стороны: если существует такой функциональный язык, как Dafny (от Microsoft), я был бы рад попробовать его.

Редактировать: Если нет способа сделать это, пожалуйста, ответьте, указав именно это. В этом случае я бы создал инструмент командной строки, который отфильтровывает эти предупреждения. (Но это, к сожалению, стерло бы все выполненное форматирование …)

Как вы, скорее всего, знаете, вы можете написать что-то вроде этого:

 let name = function
    | [a; b; ... ] -> { ... }
    | _ -> failwith "not possible"
  

Но вы можете (если настаиваете) отключить предупреждение, написав [@warning "-8"] между let и именем функции.

 $ cat warn.ml
let f [a; b] = a   b
$ ocamlc -c warn.ml
File "warn.ml", line 1, characters 6-20:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(_::_::_::_|_::[]|[])

$ cat nowarn.ml
let [@warning "-8"] f [a; b] = a   b
$ ocamlc -c nowarn.ml
$ 
  

Обновить

Я нашел способ снова включить предупреждения для тела функции, хотя это выглядит неуклюже:

 $ cat semiwarn.ml
let [@warning "-8"] f [a; b] =
    begin [@warning " 8"]
    let a' =
    match a with
        | 0 -> 14
        | 1 -> 15
    in
    a'   b
    end
$ ocamlc -c semiwarn.ml
File "semiwarn.ml", line 4, characters 4-52:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
2
  

Как вы можете видеть, в теле функции есть предупреждение о совпадении, но не для параметров функции.

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

С другой стороны: если существует такой функциональный язык, как Dafny (от Microsoft), я был бы рад попробовать его.

Система типов OCaml достаточно мощна, чтобы выразить этот тип инварианта: вы можете определять списки с индексом длины с помощью GADTs.

Вы должны начать с введения натуральных чисел на уровне типа:

 type zero    = Zero
type 'a succ = Succ
  

Это не совсем натуральные числа уровня типа, потому что вы можете писать бессмысленные выражения типа int list succ , но они достаточно близки для нашей цели: конструкторы данных нашего типа списков с индексом длины будут обеспечивать, чтобы длина состояла только из succ s и a zero в конце. Мне также пришлось предоставить каждому из этих типов конструктор по причинам, выходящим за рамки этого ответа.

Затем вы можете определить ('a, 'n) vector тип 'a list файлов, которые имеют точную длину 'n , вот так:

 type ('a, _) vector =
  | []   : ('a, zero) vector
  | (::) : 'a * ('a, 'n) vector -> ('a, 'n succ) vector
  

Используя [] и (::) в качестве конструкторов, вы получаете возможность повторно использовать list синтаксис при определении param . Я хотел бы, чтобы это было возможно записать (int, 4) vector , но я не смог найти способ сделать это.

 let param : (int, zero succ succ succ succ) vector = [3;1;0;4]
  

В качестве альтернативы, вы можете позволить OCaml выводить этот параметр, как в param_ . Вы явно не указываете инвариант, но он будет проверяться в каждой точке использования.

 let param_ : (int, _) vector = [3;1;0;4]
let () = match param_ with
 (*  [x;y;z] -> print "Argh!n" (* This doesn't typecheck *)*)
  [x;y;z;t] -> print_string "Yeah!n"