Можно ли реализовать индексированные по значению типы данных в OCaml / ReasonML? - PullRequest
Новая
       38

Можно ли реализовать индексированные по значению типы данных в OCaml / ReasonML?

1 голос
/ 10 февраля 2020

Недавно я познакомился с agda, и это привлекло мое внимание: 

data Vector (A : Set) : Nat → Set where
  []  : Vector A zero
  _∷_ : {n : Nat} → A → Vector A n → Vector A (suc n)

_++_ : ∀ {a m n} {A : Set a} → Vec A m → Vec A n → Vec A (m + n)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

Я пытался реализовать этот тип массива в OCaml, но понял, что не могу индексировать типы по значениям. Мне удалось использовать типы для длины, но я не могу применить проверку конкатенации Vec A m → Vec A n → Vec A (m + n).

Это выполнимо?

1 Ответ

3 голосов
/ 10 февраля 2020

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

Отправной точкой является определение конструкции типа для представления оператора succ 

type 'a succ = private Succ

Тогда хорошее и классическое определение натурального числа Пеано - 

type ('x,'x_plus_n) nat =
  | Zero: ('n, 'n) nat (* n + 0 = n *)
  | Succ: ('x,'x_plus_n) nat -> ('x, 'x_plus_n succ) nat
  (* succ ( n + x ) = n + succ x *)
let zero = Zero
let one = Succ zero

Преимущество этого представления в том, что сложение можно определить, указав, что добавление x + y к n может быть разложено на (n + x) + y: 

let rec (+): type n n_plus_x n_plus_x_plus_y.
(n,n_plus_x) nat -> (n_plus_x, n_plus_x_plus_y) nat -> (n,n_plus_x_plus_y) nat =
fun x y -> match y with
| Zero -> x
| Succ y -> Succ( x + y )

let two = one + one

Из них определение списка с индексом длины - это просто вопрос хранения этой естественной целочисленной кодировки внутри типа списка: 

type ('elt,'x,'x_plus_length)  nlist =
  | []: ('elt, 'n,'n) nlist
  | (::) : 'elt * ('elt, 'n, 'n_plus_length) nlist
     -> ('elt, 'n,'n_plus_length succ) nlist

Здесь мы используем тот факт, что :: является конструктором инфиксного типа и что [1;2;3] является просто некоторой синтаксией c сахар для 1 :: 2 :: 3 :: [], что означает, что мы можем написать 

let l = [1;2;3]
let l' = [1;2]

и что l=l' завершится неудачно с ошибкой типа.

С этим определением можно получить возвращенную типизированную длину с помощью просто 

let rec len: type inf sup. ('elt, inf,sup) nlist -> (inf,sup) nat =
  function
  | [] -> Zero
  | _ :: q -> Succ (len q)

и объединение двух списков требуют лишь немного утонченности, чтобы определить порядок аргументов типа: 

let rec (@): type inf mid sup.
  ('elt,mid,sup) nlist -> ('elt,inf,mid) nlist -> ('elt, inf,sup) nlist =
fun left right -> match left with
  | [] -> right
  | a :: q -> a :: (q @ right)

На самом деле главное препятствие для использования такого рода списков ts - это ограничение значения, которое делает болезненным сохранение всех задействованных переменных типа generi c (и не слабо polymorphi c).

...