我目前正在尝试使用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) **)
任何反馈都表示赞赏 . 谢谢 .
1 回答
你应该写一个递归函数来搜索:
我不知道你的所有情况是什么样的,但你会写一个像上面这样的函数 .
然后看看你是否可以统一事物:
您现在可以通过熟悉的列表功能实现您想要的功能 .