Есть ли способ использовать систему типов OCaml для обеспечения соблюдения правил о значениях? - PullRequest
Новая
       18

Есть ли способ использовать систему типов OCaml для обеспечения соблюдения правил о значениях?

3 голосов
/ 26 марта 2019

Я новичок в OCaml и изучаю возможности системы типов.У меня два вопроса.

  1. В этом типе записи есть ли способ использовать систему типов OCaml для обеспечения соблюдения правила, что nums1 + nums2 = all_nums?
type foo = {all_nums: int list; nums1: int list; nums2: int list;} ;;

например, если nums1 = [1] и nums2 = [2;3] тогда all_nums должен быть [1;2;3].

В этом типе записи есть способ принудительно использовать систему типов, чтобы ни один элемент в nums1 не должен быть также в nums2, т.е. их пересечение должно быть пустым? 
type bar = {nums1: int list; nums2: int list;} ;;

например, еслиnums1 = [1], nums2 также не может содержать 1.

Заранее спасибо.

1 Ответ

4 голосов
/ 26 марта 2019

Да и нет.Тип, который зависит от значения времени выполнения, называется зависимым типом , и OCaml не поддерживает зависимые типы в полной мере.Обычные языки программирования не поддерживают их, поскольку они делают программирование довольно громоздким.Например, теоретически, у OCaml достаточно зависимой типизации для поддержки вашего случая, за исключением того, что вы не сможете использовать list или int, и вам придется использовать GADT-представление для них.И в конце концов, это вряд ли будет полезно.Потому что система типов OCaml все еще статична, поэтому она должна проверить, что ваша программа действительна для всех возможных наборов перед ее выполнением.Это сильно ограничит набор типизированных программ.

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

Используя ваш первый пример, 

 module Foo : sig 
   type t 
   val create : int list -> int list -> int list -> (t,error) result
 end = struct 
   type t = {all_nums: int list; nums1: int list; nums2: int list;}
   type error = Broken_invariant
   let create all_nums nums1 nums2 = 
      if invariant_satisfied all_nums nums1 nums 2 
      then Ok {all_nums; nums1; nums2}
      else Error Broken_invariant
 end

Используя это запечатанное представление, невозможно создать вне модуля Foo значение типа Foo.t, для которого invariant_satisfiedне true.Следовательно, ваше Foo - это доверенное ядро ​​- единственное место, где вам нужно проверить, сохраняется ли инвариант.Система типов позаботится обо всем остальном.

Вы можете кодировать гораздо более сложные инварианты и быть более выразительными, если будете использовать фантомные типы, например, 

 module Number : sig 
     type 'a t 
     type nat
     type neg
     type any = (nat t, neg t) Either.t


     val zero : nat t
     val one : nat t
     val of_int : int -> any
     val padd : nat t -> nat t -> nat t 
     val gadd : 'a t -> 'b t -> any
 end = struct 
     type 'a t = int 
     type nat 
     type neg
     type any = (nat t, neg t) Either.t

     let zero = 0
     let one = 1
     let of_int x = if x < 0 then Right x else Left x
     let padd x y = x + y (* [see note 2] *)
     let gadd x y = of_int (x + y)
 end

, где тип Either.t определен как type ('a,'b) t = Left of 'a | Right of 'b

Примечания

Примечание 1. Ваш первый пример может быть закодирован таким образом, что невозможно разбить инвариант, например, вместо дублирования ваших данных в all_nums, вы можетепредставьте ваши типы {nums1 : int list; nums2 : int list} и определите all_nums как функцию, let all_nums = List.append

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

...