Когда полезно двойное принуждение?

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)

где f_link_type это тип f_link функция.

Причина, по которой он может потерпеть неудачу, описана в руководстве:

Бывший оператор иногда не сможет привести выражение expr из типа typ1 к типу typ2 даже если тип typ1 это подтип типа typ2: в текущей реализации он расширяет только два уровня аббревиатур типов, содержащих объекты и / или полиморфные варианты, сохраняя только рекурсию, когда это явно в типе класса (для объектов). В качестве исключения из приведенного выше алгоритма, если оба предполагаемых типа expr а также typ являются наземными (то есть не содержат переменных типа), первый оператор ведет себя как последний, принимая выводимый тип expr как typ1, В случае неудачи с первым оператором, следует использовать последний.

Позвольте мне попытаться выразить это более простыми словами. Принуждение возможно только в том случае, если известны как домен, так и кодомен. Тем не менее, во многих случаях вы можете применить эвристику, которая выведет домен из домена и текущий тип выражения. Эта эвристика работает, если тип выражения является наземным, не имеет рекурсий и некоторых других ограничений. По сути, если тип домена не имеет уникального наиболее общего типа, нам нужно перечислить все возможные обобщения и проверить каждую возможную комбинацию.