ocaml полиморфный вариант тип предполагаемый тип слишком общий

Question

У меня есть этот код

let my_fun: [`X | `Y | `Z] -> [`Z | `Y] = function
  | `X -> `Y
  | x -> x

Он не компилируется с сообщением

11 |   | x -> x
          ^
Error: This expression has type [ `X | `Y | `Z ]
       but an expression was expected of type [ `Y | `Z ]
       The second variant type does not allow tag(s) `X

Почему комплимент не может определить тип [Z |Y], если ясно, что `X никогда не может быть возвращен из функции?

Answer 1

Почему компилятор не может вывести тип [Z |Y], если ясно, что `X никогда не может быть возвращен из функции?

Более простой пример:

if false then 0 else "hello"

Компилятор должен отклонить его, потому что для набора текста на языках ML требуется, чтобы обе ветви имели один и тот же тип ¹, а типы int а также stringневозможно объединить; это верно, даже если вы могли бы сказать, что нет никаких шансов, что выражение когда-либо могло быть оценено как 0 (однако имейте в виду, что формально говоря, нет смысла говорить, что мы оцениваем выражение, которое не является частью языка, как определено).

В matchвыражение, типы левой части всех предложений должны соответствовать типу сопоставляемого выражения. Такx в последнем предложении имеет тот же тип, что и неявный аргумент в function, который является типом ввода, объявленным в подписи. Это правда, независимо от того,`X является допустимым значением в этом контексте.

Вам необходимо перечислить все допустимые случаи; если вам это нужно часто в вашем коде, вам лучше написать для этого специальную функцию:

let f : ([> `Y | `Z ] -> [`Y | `Z ] option) = function
  | (`Y|`Z) as u -> (Some u) 
  | _ -> None;

Например:

# f `O;;
- : [ `Y | `Z ] option = None
# f `Y;;
- : [ `Y | `Z ] option = Some `Y

См. Также теоретико-множественные типы для полиморфных вариантов ^(pdf)

---

[1] Для сравнения, в Common Lisp, который имеет динамическую типизацию, эквивалентное выражение является допустимым; статический анализ, выполняемый компилятором SBCL, может определить его тип, то есть строку длиной 5:

> (describe (lambda () (if nil 0 "hello")))
....
Derived type: (FUNCTION NIL
               (VALUES (SIMPLE-ARRAY CHARACTER (5)) &OPTIONAL))

Answer 2

Если тип x было выведено быть [`Y | `Z], то его нельзя использовать в типе [`X | `Y | `Z] что было бы странно, поскольку он привязан к аргументу этого типа.

Вы можете использовать as шаблоны, чтобы получить привязку с уточненным типом, например:

let my_fun: [`X | `Y | `Z] -> [`Y | `Z] = function
  | `X -> `Y
  | (`Y | `Z) as yz -> yz

В #type_name шаблоны могут быть очень полезны, если вы хотите сделать это для полиморфных вариантов с большим количеством случаев.