是否可以在 OCaml/ReasonML 上实现值索引数据类型？

Question

最近有人介绍我使用 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)。

可行吗？

Answer 1

OCaml 不支持依赖类型，因此不可能有值索引类型。但是，对于长度索引列表，仅使用 GADT 可能会走得很远。

起点是定义一个类型构造来表示 succ 运算符

type 'a succ = private Succ

那么Peano自然数的一个很好的经典定义是

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] 只是 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)

事实上，使用这类列表的主要障碍是值限制，这使得保持所有类型变量涉及泛型（而不是弱多态）变得很痛苦。

是否可以在 OCaml/ReasonML 上实现值索引数据类型？

Is it possible to implement value-indexed data types on OCaml/ReasonML?

ocaml

types

agda