OCaml 检查元组右侧是否存在元素答案

【问题标题】：OCaml checking if an element exists on the right-hand side of a tupleOCaml 检查元组右侧是否存在元素
【发布时间】：2018-12-10 10:09:33
【问题描述】：

我目前正在尝试使用 OCaml 语言实现类型推断算法（统一算法）。我遇到了一些实施方面的困难，希望有人能给予我一些帮助。

让我提供一些我正在尝试实现的背景信息。

[(TypeVar "t1", TypeFunc (TypeVar "t2", TypeVar "t3"))]

(type * type) list 类型是一种表达相等性的方式，因此类型 t1 映射到 t2 -> t3 的函数。

我试图捕捉的是等式左侧的类型变量也出现在右侧的情况，这会导致算法失败。详细地说，如果我们有

[(TypeVar "t1", TypeFunc (TypeVar "t1", TypeVar "t3"))]

这会给我们一个错误，因为t1 = t1 -> t3 是矛盾的。

这是我试图实现的实际 OCaml 函数来捕捉这个矛盾：

let contradiction_check (a, t) =
  List.exists (fun (x, _) -> x = a) t;;

let t1 = TypeVar "t1";;
let t2 = TypeFunc (TypeVar "t2", TypeVar "t3");;

这段代码的问题在于，首先t2 不是一个列表，这会给我们一个错误。但是，这是故意的，因为我的目标是获取元组列表 [(TypeVar "t1", TypeFunc (TypeVar "t2", TypeVar "t3"))] 并检查元组的左侧是否出现在右侧。

我想我的具体问题是：是否可以将 List.exists 函数实现为元组的版本？我尝试过手动编写函数，但它似乎比我最初想象的要复杂。

对于以下示例，它变得特别复杂：

[(TypeVar "t1", TypeFunc (TypeFunc (TypeVar "t2", TypeVar "t3"),
  TypeFunc (TypeVar "t1", TypeVar "t4")))]

(** t1 = (t2 -> t3) -> (t1 -> t4) **)

感谢任何反馈。谢谢。

【问题讨论】：

标签： list tuples ocaml type-inference

【解决方案1】：

你应该只写一个递归函数来搜索：

(** [is_free ~varname t] is [true] iff [varname] appears as a free type variable in [t] *)
let is_free ~varname =
  let rec r = function
    | TypeVar n when String.( = ) n varname -> true
    | TypeVar _ -> false
    | TypeFunc s t -> r s || r t
    | TypaApp c t -> r c || r t (* if c is just a name not a type you don’t want [r c] here *)
    | TypeForall n t -> 
      if String.( = ) n varname
      then false
      else r t
  in
  r

我不知道你所有的案例是什么样的，但你会写一个类似上面的函数。

那就看看能不能统一一下：

let can_unify = function
  | TypeVar t1, TypeVar t2 when String.( = ) t1 t2 -> (* decide what to do here *)
  | TypeVar varname, t -> not (is_free ~varname t)
  | _ -> (* throw an error or fix your types so this case can’t happen *)

您现在可以使用熟悉的列表函数实现您想要的功能。

【讨论】：