OCaml如何在异构列表上实现交换？

Question

我正在关注本教程https://drup.github.io/2016/08/02/difflists/

并尝试在异构列表上实现交换，但它不进行类型检查

type ('ty, 'v) t =
  | Nil : ('v, 'v) t
  | Cons : 'a * ('ty, 'v) t -> ('a -> 'ty, 'v) t

let plus1 l = Cons ((), l) (* : ('a, 'b) t -> (unit -> 'a, 'b) t *)
let one x = Cons (x, Nil) (* : 'a -> ('a -> 'b, 'b) t *)
let l1 = Cons (1, Cons ("bla", Nil)) (* : (int -> string -> 'a, 'a) t *)
let l2 = Cons ((), Cons (true, Nil)) (*: (unit -> float -> 'a, 'a) t *)
let l3 = Cons (1, Cons ("bla", Cons ((), Cons (true, Nil)))) (*: (int -> string -> unit -> float -> 'a, 'a) t *)

let rec append
  : type ty1 ty2 v.
    (ty1, ty2) t ->
    (ty2, v) t ->
    (ty1, v) t =
  fun l1 l2 -> match l1 with
  | Nil -> l2
  | Cons (h, t) -> Cons (h, append t l2)

let l4 = Cons (1, Cons ("bla", Nil)) (* : (int -> string -> 'a, 'a) t *)
let l5 = Cons ("bla", Cons (1, Nil)) (* : (string -> int -> 'a, 'a) t *)

let swap
  : type ty1 ty2 v. 
  (ty1 -> ty2 -> v, v) t ->
  (ty2 -> ty1 -> v, v) t =
  function
  | Nil -> Nil
  | Cons (a, Cons (b, tl)) -> Cons (b, Cons (a, tl))
  | Cons (a, Nil) -> Cons (a, Nil)

我明白了

Error: This expression has type (ty2 -> ty1 -> v, ty2 -> ty1 -> v) t
       but an expression was expected of type (ty2 -> ty1 -> v, v) t
       Type ty2 -> ty1 -> v is not compatible with type v 

在该 | Nil -> Nil行中，我知道类型不匹配，但不知道从这里去哪里

如果我尝试

Error: This expression has type (ty2 -> ty1 -> v, ty2 -> ty1 -> v) t
       but an expression was expected of type (ty2 -> ty1 -> v, v) t
       Type ty2 -> ty1 -> v is not compatible with type v 

我收到此警告

File "./difflist.ml", lines 27-28, characters 2-52:
27 | ..function
28 |   | Cons (a, Cons (b, tl)) -> Cons (b, Cons (a, tl))
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Cons (_, Nil)

同样Nil，我可以做到这一点，但似乎并不理想

let swap
  : type ty1 ty2 v. 
  (ty1 -> ty2 -> v, v) t ->
  (ty2 -> ty1 -> v, v) t =
  function
  | Cons (a, Cons (b, tl)) -> Cons (b, Cons (a, tl))

我不能将其称为小于预期的 2 的列表。我希望由于类型检查器可以检测到类型错误的调用，因此它不会抱怨匹配不详尽

如果我尝试与我进行匹配，assert false则会出现这些错误（这是预期的）

File "./difflist.ml", lines 27-28, characters 2-52:
27 | ..function
28 |   | Cons (a, Cons (b, tl)) -> Cons (b, Cons (a, tl))
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Cons (_, Nil)

有什么办法可以摆脱这些assert false吗？

Answer 1

问题是交换函数仅针对长度大于 2 的列表定义，并且 difflist 异构列表不会在类型级别对长度进行编码。事实上，类型列表(ty->ty2->mid,last) t可以有任意长度。例如，

let t: (int -> float -> int, int -> float -> int) t = Nil

已验证。

因此，一种选择是返回一个选项类型，例如同质列表，None如果列表长度太小则返回：

let swap
  : type ty1 ty2 v tl.
  (ty1 -> ty2 -> v, tl) t ->
  (ty2 -> ty1 -> v, tl) t option =
  function
  | Nil -> None
  | Cons(_,Nil) -> None
  | Cons (a, Cons (b, tl)) -> Some(Cons (b, Cons (a, tl)))

另一种选择是通过修复尾部类型来关闭列表以进一步扩展：

type void = |
let swap
  : type ty1 ty2 tl.
  (ty1 -> ty2 -> tl, void) t ->
  (ty2 -> ty1 -> tl, void) t =
  function
  | Cons (a, Cons (b, tl)) -> Cons (b, Cons (a, tl))
  | _  -> .
  | Cons(_,_) -> .

在这里，我使用空类型作为尾部类型，因为该类型不链接到任何值的类型，但任何其他地面类型都可以工作。