Блог

Я довольно новичок в 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].

2. В этом типе записи есть ли способ принудительно использовать систему типов, чтобы ни один элемент в nums1 не был также в nums2, т. Е. их пересечение должно быть пустым?

 type bar = {nums1: int list; nums2: int list;} ;;
  

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

Заранее благодарю вас.

Да и нет. Тип, который зависит от значения во время выполнения, называется зависимым типом, а OCaml не поддерживает зависимые типы в полной мере. Для обычных языков программирования нетипично поддерживать их, поскольку они делают программирование довольно громоздким. Например, теоретически, OCaml имеет достаточно зависимой типизации для поддержки вашего случая, за исключением того, что вы не сможете использовать list or 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, как и многие другие языки программирования, использует модульную арифметику, сложение двух положительных чисел может привести к отрицательному числу, поэтому наш пример неудачный. Но для примера давайте проигнорируем это 🙂