types - 双重强制什么时候有用？

Question

我在 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无法转换为类型 tfull .

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

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

Answer 1

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

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

<subtype> type 有时可以省略，在这种情况下，它被称为单一强制。因此，在您的情况下，正确的强制转换应如下所示:

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

哪里 f_link_type是 f_link 的类型功能。

可能失败的原因在 the manual中描述。 :

The former operator will sometimes fail to coerce an expression expr from a type typ1 to a type typ2 even if type typ1 is a subtype of type typ2: in the current implementation it only expands two levels of type abbreviations containing objects and/or polymorphic variants, keeping only recursion when it is explicit in the class type (for objects). As an exception to the above algorithm, if both the inferred type of expr and typ are ground (i.e. do not contain type variables), the former operator behaves as the latter one, taking the inferred type of expr as typ1. In case of failure with the former operator, the latter one should be used.

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