Как использовать GADT для модулей в OCaml без предупреждения?

Question

У меня есть два файла: gadt1.ml и gadt2.ml, а второй зависит от первого.

gadt1.ml:

type never 
type _ t1 = A1 : never t1 | B1 : bool t1 
type _ t2 = A2 : string t2 | B2 : bool t2 
let get1 : bool t1 -> bool = function B1 -> true 
let get2 : bool t2 -> bool = function B2 -> true 

gadt2.ml:

let get1 : bool Gadt1.t1 -> bool = function Gadt.B1 -> true 
let get2 : bool Gadt1.t2 -> bool = function Gadt.B2 -> true 

, когда я компилирую с помощью OCaml 4.02.3 (ocamlbuild gadt2.native), я получаю предупреждение 8 о функции Gadt2.get1 не будучи исчерпывающим. Я довольно озадачен тем, что Gadt2.get1 вызывает предупреждение, а Gadt1.get1 и Gadt2.get2 - нет.

Мое предположение заключалось в том, что пустой тип never не может быть равен bool, поэтому Gadt2.get1 не должен вызывать предупреждение. С другой стороны, если я вызываю Gadt2.get1 с аргументом A1, я получаю ошибку типа (по желанию). Является ли предупреждение ожидаемым поведением или ошибкой? Что я упустил?

Кстати, добавление -principal к флагам компиляции ничего не меняет.

Answer 1

Gadt2 может видеть только интерфейс Gadt1, а не его реализацию. Интерфейс выглядит следующим образом:

type never 
type _ t1 = A1 : never t1 | B1 : bool t1 
type _ t2 = A2 : string t2 | B2 : bool t2 
val get1 : bool t1 -> bool 
val get2 : bool t2 -> bool 

Обратите внимание, что type never абстрактно - нет ничего, чтобы остановить реализацию придав ему RHS. В частности, вы можете, внутри gadt1.ml, написать type never = bool, в этот момент становится целесообразным пройти A1 до get1, и поэтому get1 необходимо подготовить для этой возможности.

В противоположность этому, string не является абстрактным типом: он имеет известное представление, поэтому он не может быть равна bool, и поэтому A2 никогда не мог быть передан get2.

Что вы, кажется, пытается сделать с never это объявить тип, который не является абстрактным, но пустой, обнажая свое представительство как не имеющие конструкторов вообще. К сожалению, это просто не поддерживается OCaml; способность определять тип, который локальный компилятор может сказать, пуст, является немного причудой, и на самом деле не упоминается в manual. Невозможно выразить «этот тип пуст» в сигнатуре модуля.

Answer 2

Как говорит Бен, проблема в том, что в сигнатуре type t является абстрактным, а не пустым. Одним из вариантов является определение типа, который необитаем:

module One = struct 
    type never = { impossible : 'a . 'a } 
    type _ t1 = A1 : never t1 | B1 : bool t1 
    type _ t2 = A2 : string t2 | B2 : bool t2 
    let get1 : bool t1 -> bool = function B1 -> true 
    let get2 : bool t2 -> bool = function B2 -> true 
end 

module Two = struct 
    let get1 : bool One.t1 -> bool = function One.B1 -> true 
    let get2 : bool One.t2 -> bool = function One.B2 -> true 
end 

Это не дает никаких предупреждений исчерпанность.