代码之家 › 专栏 › 技术社区 › geckos

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

ocaml

geckos · 技术社区 · 2 年前

我在学习这个教程 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 *)

有什么办法摆脱这些吗 断言为false ?

0 回复 | 直到 2 年前

octachron 2 年前

问题是,交换函数只为长度大于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(_,_) -> .

在这里,我使用一个空类型作为尾部的类型,因为这个类型没有链接到任何值的类型,但任何其他基础类型都可以。