Почему порядок операндов влияет на область видимости?
Я пытаюсь понять, почему определенный конструктор принимается в одном выражении, а не в другом. Я ожидал, что это будет вне сферы действия в обоих случаях. Я новичок в OCaml (в основном я использую Haskell), поэтому я мог упустить что-то совершенно очевидное для опытного человека.
type zero = Zero
type 'n succ = Succ
type 'n snat =
| SZero : zero snat
| SSucc : 'm snat -> 'm succ snat
module SimpleInduction (Pred : sig type 'n pred end) = struct
open Pred
type hyps =
{ base : zero pred
; step : 'm. 'm pred -> 'm succ pred}
let rec induct : type n. hyps -> n snat -> n pred =
fun h sn -> match sn with
| SZero -> h.base
| SSucc p -> h.step (induct h p)
end;;
let module Snot = struct type 'n pred = Top end in
let module Goop = SimpleInduction(Snot) in
Goop.induct {base = Top; step = fun _ -> Top} SZero = Top;;
(*
let module Snot = struct type 'n pred = Top end in
let module Goop = SimpleInduction(Snot) in
Top = Goop.induct {base = Top; step = fun _ -> Top} SZero;;
*)
Это компилируется просто отлично, по какой-то причине. Когда второе определение Snot раскомментировано, я получаю сообщение об ошибке:
19 | Top = Goop.induct {base = Top; step = fun _ -> Top} SZero;;
^^^
Error: Unbound constructor Top
Что вводит Top в рамки первого определения Snot? Использование обычных модулей, а не первоклассных локальных, не имеет значения.
Если я использую Snot.Top с левой стороны, я не получаю жалоб с правой стороны. Почему это?
Кроме того, немного не по делу, но все же полезно знать, что здесь не используются первоклассные модули. Существуют локальные модули и функторы, но ни один из них не является действительно первоклассным в том смысле, что их можно передавать в качестве значений обычным функциям. Модуль первого класса — это представление модуля на уровне значений, которое вы создаете, упаковывая его вместе с сигнатурой. Например. let first_class_module = (module M : MSig).
@glennsl, значит, компилятор просто помещает конструктор в область видимости, если он может сделать вывод, что я ищу что-то в этом роде?
По крайней мере, это мое понимание. Я ожидаю, что вы получите ответ с подробным объяснением механизма в течение дня или двух, как это обычно бывает :)
Ответы 1
Короче говоря, направленное на тип устранение неоднозначности действительно не ограничивается рамками.
С явной аннотацией типа средство проверки типов может выбрать конструктор из типа, не помещая конструктор в область видимости.
Например,
module M = struct type 'a t = A of 'a end
let ok: _ M.t = A ()
let wrong: _ M.t = A (A ())
первый пример действителен, потому что аннотации типа достаточно, чтобы знать, что A в A () является _ A.t. Однако второй пример не работает, потому что конструктор не попал в область видимости.
Кроме того, для устранения неоднозначности по типу требуется, чтобы был известен только ожидаемый тип конструктора или записи. Как правило, в этом примере
let expected =
let f (M.A x) = x in
f (A ())
мы знаем, что тип аргумента f является _ M.t, поэтому мы знаем, что A в f (A ()) происходит от _ M.t, и мы можем использовать устранение неоднозначности, направленное на тип, как в случае с явной аннотацией.
Если вы считаете такое поведение экзотическим, в такой ситуации можно использовать предупреждение 42 [имя вне области видимости]. Компиляция вашего примера с этим предупреждением дает (среди многих других случаев этого предупреждения)
23 | Goop.induct {base = Top; step = fun _ -> Top} SZero = Top
^^^
Warning 40 [name-out-of-scope]: Top was selected from type Snot.pred.
It is not visible in the current scope, and will not
be selected if the type becomes unknown.
(имена предупреждений новые в 4.12)
Что касается вашего второго пункта, порядок выражения может иметь значение при отсутствии явных аннотаций. Действительно, без явной аннотации устранение неоднозначности, направленное на тип, сможет выбрать правильный конструктор только тогда, когда ожидаемый тип уже известен. А проверка типов в OCaml идет слева направо. Таким образом, в
... = Top
тип левой части уже выведен, и поэтому ожидаемый тип Top равен _ Snot.pred.
Когда порядок обратный
Top = ...
средство проверки типов пытается найти конструктор Top без какой-либо информации о типе, и в области видимости нет конструктора Top. Таким образом, он терпит неудачу с ошибкой Unbound constructor. Если вы хотите избежать зависимости от порядка, вы можете либо
- напишите полное имя конструктора:
Snot.Top = ...
- использовать явную аннотацию типа
(Top: _ Snot.pred) = ...
- откройте модуль
Snot.
Snot.( Top ) = ...
(* or *)
let open Snot in Top = ...
Я бы посоветовал использовать одно из этих решений, поскольку они более надежны.
В конце концов, полагаться на конкретную реализацию проверки типов нельзя.
На самом деле, есть флаг компилятора -principal и предупреждение (18) [not-Principal], которое заботится о том, чтобы выдать предупреждение при наличии такого потенциально хрупкого вывода:
23 | Goop.induct {base = Top; step = fun _ -> Top} SZero = Top
^^^
Warning 18 [not-principal]: this type-based constructor disambiguation is not principal.
Здесь «не основной» означает, что результат устранения неоднозначности на основе типов зависел от порядка проверки типов.
Я подозреваю, что это просто выведено из типа
Goop.induct. Типы выводятся за один проход, слева направо, поэтому, когда он встречаетTopво втором определении, он понятия не имеет, чтоSnot.predзадействован.