什么时候双重强制有用？

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>可以省略该类型,在这种情况下,它被称为单个强制.所以在你的情况下,正确的强制应该是这样的:

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

where f_link_type是一种f_link函数.

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

即使type 是类型的子类型, 前一个运算符有时也无法强制expr 从类型typ1到类型的表达式:在当前实现中,它只扩展包含对象和/或多态变体的两级类型缩写,只保留递归时的类型在类类型(对象)中是显式的.作为上述算法的一个例外,如果推断的 和的类型都是基础的(即不包含类型变量),则前一个运算符的行为与后者相同,采用推断类型 as .如果前操作员出现故障,应使用后者.typ2typ1typ2exprtypexprtyp1

让我试着用更简单的术语来表达.只有在知道域和域的情况下才能进行强制.但是,在许多情况下,您可以应用一种启发式方法,该方法将从codomain和当前表达式中推断出域.如果表达式的类型是基础的,没有递归和一些其他限制,则此启发式工作.基本上,如果域类型没有唯一最通用的类​​型,我们需要枚举所有可能的概括并检查每个可能的组合.