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 行，我知道类型不匹配，但不知道从这里去哪里

如果我尝试

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))

我收到此警告

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))
  | Cons (_, Nil) -> assert false
  | Nil -> assert false

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

如果我尝试使用 assert false 进行匹配，我会收到这些错误(这是预期的)

let l7 = swap Nil
(* This expression has type ('a -> 'b -> 'c, 'a -> 'b -> 'c) t
but an expression was expected of type ('a -> 'b -> 'c, 'c) t
The type variable 'd occurs inside 'e -> 'f -> 'd *)
let l8 = swap (Cons (true, Nil))
(* This expression has type ('a -> 'b, 'a -> 'b) t
but an expression was expected of type ('a -> 'b, 'b) t
The type variable 'c occurs inside 'd -> 'c *)

有什么办法可以摆脱这些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(_,_) -> .

这里我使用空类型作为尾部类型，因为该类型没有链接到任何值的类型，但任何其他基本类型都可以。