双重强制何时有用？

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)

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

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

谁能给我解释一下为什么不能直接将 f_link 强制转换为 tfull，但是可以将其强制转换为 tfull 间接使用 tphrasing 作为中间步骤？

也欢迎任何指向它背后的类型理论的指针。

Answer 1

通用强制转换运算符，也称为双重强制转换，具有以下形式

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

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

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.

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

双重强制何时有用？

When is double coercion useful?

ocaml

types

coercion

ocsigen