7

我在 OCaml 中偶然发现了以下编译消息：

This simple coercion was not fully general. Consider using a double coercion.

它发生在一个相当复杂的源代码中，但这里是一个 MNWE：

open Eliom_content.Html.D

let f_link s =
  let arg : Html_types.phrasing_without_interactive elt list = [pcdata "test"] in
  [ Raw.a ~a:[a_href (uri_of_string (fun () -> "test.com"))] arg ]

type tfull = (string -> Html_types.flow5 elt list)
type tphrasing = (string -> Html_types.phrasing elt list)

let a : tfull = ((f_link :> tphrasing) :> tfull)

let b : tfull = (f_link :> tfull)

ocamlfind ocamlc -c -package eliom.server -thread test.ml您可以使用安装了 Eliom 6的 编译此示例。

错误发生在最后一行，OCaml 编译器抱怨f_link无法转换为 type tfull。

有人可以向我解释为什么不能直接强制f_link，tfull但可以强制它tfull间接tphrasing用作中间步骤吗？

任何指向其背后的类型理论的指针也将受到欢迎。

4

1 回答 1

9

一般强制运算符，也称为双重强制，有一个形式

(<exp> : <subtype> :> <type>)

有时<subtype>可以省略类型，在这种情况下，它称为单一强制。所以在你的情况下，正确的强制应该是这样的：

let a : tfull = (f_link : f_link_type :> tfull)

wheref_link_type是f_link函数的类型。

手册中描述了它可能失败的原因：

即使 type是 type 的子类型，前一个运算符有时也无法将表达式expr 从一个类型强制转换为typ1一个类型：在当前实现中，它只扩展了包含对象和/或多态变体的两个级别的类型缩写，当它只保留递归时在类类型中是显式的（对于对象）。作为上述算法的一个例外，如果 和 的推断类型 都是接地的（即不包含类型变量），则前一个运算符的行为与后一个运算符一样，将推断类型为 as 。如果前一个运算符出现故障，则应使用后一个运算符。typ2typ1typ2exprtypexprtyp1

让我试着用更简单的术语来表达。仅当域和共域都已知时，才可能进行强制转换。但是，在许多情况下，您可以应用启发式方法，从共域和当前表达式类型推断域。如果表达式的类型是基本的、没有递归和一些其他限制，则这种启发式方法有效。基本上，如果域类型没有唯一的最通用类型，我们需要枚举所有可能的概括并检查每个可能的组合。

于 2017-06-09T08:20:43.160 回答