Полиморфные варианты и let%bind type error

Question

Полиморфные варианты и let%bind type error

Я пытаюсь использовать технику составной обработки ошибок в OCaml (тип результата с полиморфными вариантами ошибок) для некоторого кода, который я написал. Типы функций, которые я пытаюсь использовать, выглядят так:

val parse : parser -> token list -> (Nominal.term, [> `ParseError of string ]) Result.t
val lex : lexer -> string -> (token list, [> `LexError of string ]) Result.t

Моя попытка составить их такова:

let lex_and_parse
  : parser -> lexer -> string -> (Nominal.term, [> `ParseError of string | `LexError of string ]) Result.t
  = fun parser lexer input ->
    let open Result.Let_syntax in
    let%bind tokens = lex lexer input in
    parse parser tokens

К сожалению, компилятор (4.09.0) сообщает об ошибке типа:

File "src/Pratt.ml", line 147, characters 4-23:
147 |     parse parser tokens
          ^^^^^^^^^^^^^^^^^^^
Error: This expression has type
         (Nominal.term, [ `ParseError of string ]) result
       but an expression was expected of type
         (Nominal.term, [> `LexError of string ]) result
       The first variant type does not allow tag(s) `LexError

Обратите внимание: если я сделаю аналог вручную, код компилируется:

let lex_and_parse
  : parser -> lexer -> string -> (Nominal.term, [> `ParseError of string | `LexError of string ]) Result.t
  = fun parser lexer input ->
    match lex lexer input with
      | Error (`LexError err) -> Error (`LexError err)
      | Ok tokens ->
        (match parse parser tokens with
        | Ok result -> Ok result
        | Error (`ParseError err) -> Error (`ParseError err))

На самом деле это не совсем так. Эквивалент этого, который также не компилируется (таким же образом):

    match lex lexer input with
      | Error err -> Error err
      | Ok tokens ->
        match parse parser tokens with
        | Ok result -> Ok result
        | Error err -> Error err

File "src/Pratt.ml", line 155, characters 29-32:
155 |         | Error err -> Error err
                                   ^^^
Error: This expression has type [ `ParseError of string ]
       but an expression was expected of type
         [> `LexError of string | `ParseError of string ]
       The first variant type does not allow tag(s) `LexError

Итак, мой вопрос такой. Обратите внимание, что в сообщении об ошибке говорится: "Это выражение имеет тип(Nominal.term, [ `ParseError of string ]) result". Вот чего я не понимаю - я нигде не указываю этот тип, фактически, в обоих местах ParseError упоминается, это с >ограничение. Так откуда появился этот тип? IE где же[>ParseError строки]become[ ParseError of string ]?

Также:

В чем разница между моей попыткой и оригиналом Владимира (который, как я полагаю, компилируется)?
Есть ли способ ослабить полиморфный вариант из [ x ] к [> x ]? (кроме ручного сопоставления всех тегов от первого типа ко второму)

Редактировать:

Я загрузил весь свой код для контекста.

Изменить 2 (извините):

Я провел небольшое исследование и придумал такую реализацию:

let parse : parser -> token list -> (Nominal.term, [> `ParseError of string ]) Result.t
  = fun parser toks ->
    match expression parser toks with
    (* | [], result -> result *)
    (* | _, Error err -> Error err *)
    | _, Ok _ -> Error (`ParseError "leftover tokens")
    | _, _ -> Error (`ParseError "unimplemented")

Если я удалю любую из закомментированных строк, реализацияlex_and_parseснова начинает терпеть неудачу. Меня немного беспокоит то, чтоparseкомпилируется, и его сигнатура типа никогда не изменяется, но вызывающая сторона может не выполнить проверку типа. Как это возможно? Такой нелокальный эффект серьезно нарушает мои ожидания относительно того, как (должны) работать проверка типов / подписи. Очень хотелось бы понять, что происходит.

0

ocaml polymorphic-variants

Источник

user383958 02 июн '20 в 18:43

2 ответа

Решение

Следующий функторизованный код:

module F(X: sig
    type parser type lexer type token
    module Nominal: sig type term end
    val parse :
      parser -> token list -> (Nominal.term, [> `ParseError of string ]) Result.t
    val lex : lexer -> string -> (token list, [> `LexError of string ]) Result.t
end) = struct
open X

let (let*) x f = match x with
  | Error _ as e -> e
  | Ok x -> f x

let lex_and_parse parser lexer input =
  let* tokens = lex lexer input in
  parse parser tokens
end

отлично компилируется с ожидаемым типом для lex_and_parse.

Таким образом, проблема, вероятно, в том, что ваша реализация parse а также lex имеют закрытый тип ошибки.

Обратите внимание, что эту проблему можно легко исправить с помощью принуждения, поскольку закрытый тип ошибки является подтипом открытого:

let fix parse =
(parse:
    parser -> token list -> (Nominal.term, [`ParseError of string ]) Result.t
 :> parser -> token list -> (Nominal.term, [>`ParseError of string ]) Result.t
 )

но, наверное, лучше исправить реализацию соответствующих функций.

РЕДАКТИРОВАТЬ:

Первоначальная ошибка возникает из этой части вашего кода:

type parse_error = [ `ParseError of string ]
type parse_result = (Nominal.term, parse_error) Result.t
...
let rec expression
  : parser -> ?rbp:int -> token list -> token list * parse_result
...
let parse :
  parser -> token list -> (Nominal.term, [> `ParseError of string ]) Result.t
  = fun parser toks -> match expression parser toks with
    | [], result -> result

Здесь вы ограничиваете ошибку в parse_error типа быть точно `Parse_error. Таким образом, когда вы вернетесьresult в parse, его тип его (_,parse_error) result. И поскольку этот тип результата может быть объединен с вашей аннотацией, ошибки не возникает.

Возможно, первое исправление состоит в том, чтобы детализировать тип, чтобы программа проверки типов знала, что вы хотите, чтобы тип ошибки был открытым:

let parse : 'error.
  parser -> token list -> 
  (Nominal.term, [> `ParseError of string ] as 'error) Result.t
  = fun parser toks -> match expression parser toks with
    | [], result -> result

Здесь явная универсальная аннотация для возвращаемого типа предотвратит закрытие типа за вашей спиной (сообщение об ошибке могло сбивать с толку до 4.10).

Затем одно из возможных исправлений - добавить принуждение, чтобы повторно открыть тип ошибки при синтаксическом анализе:

let parse : 'error.
  parser -> token list ->
  (Nominal.term, [> `ParseError of string ] as 'error) Result.t
  = fun parser toks -> match expression parser toks with
    | [], result -> (result:>(Nominal.term, [> parse_error]) result)

или вы также можете открыть выражение типа ошибки:

type parse_error = [ `ParseError of string ]
type 'a parse_result = (Nominal.term, [> parse_error] as 'a) Result.t
...
let rec expression
  : parser -> ?rbp:int -> token list -> token list * 'a parse_result
  = ...

Или еще более простое решение: удалите аннотацию типа с помощью

let rec expression parser ... =

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

2

Источник

user7369366 02 июн '20 в 19:39

Другие вопросы по тегам ocaml polymorphic-variants

user2625442 02 июн '20 в 19:59 2020-06-02 19:59 · Accepted Answer · 2020-06-02 19:59

Итак, во-первых, ваша интуиция верна, ваш код должен работать, например, следующий код принимается 4.09.0 без каких-либо ошибок типа:

open Base

module type S = sig
  type parser
  type lexer
  type token
  type term

  val parse : parser -> token list -> (term, [> `ParseError of string ]) Result.t
  val lex : lexer -> string -> (token list, [> `LexError of string ]) Result.t
end

module Test (P : S) = struct
  open P
  let lex_and_parse :
    parser -> lexer -> string -> (term, [> `ParseError of string | `LexError of string ]) Result.t
    = fun parser lexer input ->
      let open Result.Let_syntax in
      let%bind tokens = lex lexer input in
      parse parser tokens
end


module PL : S = struct
  type parser
  type lexer
  type token
  type term

  let parse _parser _tokens = Error (`ParseError "not implemented")
  let lex _ _ = Error (`LexError "not implemented")
end

Итак, мой вопрос такой. Обратите внимание, что в сообщении об ошибке говорится: "Это выражение имеет тип (Nominal.term, [ `ParseError of string ]) result". Вот чего я не понимаю - я нигде не указываю этот тип, фактически, в обоих местах, где упоминается ParseError, это с ограничением>. Так откуда появился этот тип? IE, где [>ParseError строки] становится [ ParseError строки]?

Вы правы, это главный виновник. По какой-то причине вашparse функция возвращает значение типа

(term, [`ParseError of string])

где тип составляющей ошибки является наземным типом, т. е. не полиморфен и не может быть расширен. Трудно сказать, почему это произошло, но я уверен, что должна быть какая-то аннотация типа, которую вы поместили, которая не позволяет средству проверки типов выводить наиболее общий тип дляparseфункция. В любом случае виновник где-то скрывается, а не в том коде, который вы нам показали.

Есть ли способ ослабить полиморфный вариант с [ x ] до [> x ]? (кроме ручного сопоставления всех тегов от первого типа ко второму)

Да,

# let weaken x = (x : [`T]  :> [> `T]);;
val weaken : [ `T ] -> [> `T ] = <fun>

В чем разница между моей попыткой и оригиналом Владимира (который, как я полагаю, компилируется)?

Фактически ваша функция синтаксического анализа возвращает нерасширяемый тип. Обратите внимание: чтобы превратить нерасширяемый тип в расширяемый, вы должны использовать приведение полной формы, например, если вы определитеlex_and_parse в качестве

  let lex_and_parse :
    parser -> lexer -> string -> (term, [> `ParseError of string | `LexError of string ]) Result.t
    = fun parser lexer input ->
      let open Result.Let_syntax in
      let parse = (parse
                   :  _ -> _ -> (_, [ `ParseError of string]) Result.t
                   :> _ -> _ -> (_, [> `ParseError of string]) Result.t) in

      let%bind tokens = lex lexer input in
      parse parser tokens

он будет компилироваться. Но опять же главный виновник - это тип вашегоparse функция.

Где скрывался настоящий баг

После того, как OP загрузил исходный код, мы смогли определить, почему и где программе проверки типов OCaml было отказано в определении общего и полиморфного типа.

Вот история, parse функция реализована как

let parse : parser -> token list -> (Nominal.term, [> `ParseError of string ]) Result.t
  = fun parser toks -> match expression parser toks with
    | [], result -> result
    | _, Ok _ -> Error (`ParseError "leftover tokens")
    | _, Error err -> Error err

Таким образом, его возвращаемый тип представляет собой объединение типов следующих выражений:

result,
Error ('ParseError "leftover tokens")
Error err

кроме того, у нас есть ограничение типа

parser -> token list -> (Nominal.term, [> `ParseError of string ]) Result.t

И вот что важно понимать: ограниченный тип - это не определение, поэтому, когда вы говорите let x : 'a = 42 ты не определяешь x иметь универсальный полиморфный тип 'a. Ограничение типа(expr : typeexpr) вынуждает тип expr быть совместимым с typexpr. Другими словами, ограничение типа может ограничивать только тип, но сам тип всегда выводится по типу проверки. Если предполагаемый тип более общий, например,'a list чем ограничение, например, int list, то он будет ограничен int list. Но вы не можете двигаться в обратном направлении, так как это нарушит правильность типа, например, если предполагаемый типint list и ваше ограничение 'a list, то все равно будет 'a list(относитесь к этому как к пересечению типов). Опять же, вывод типа будет выводить наиболее общий тип, и вы можете только сделать его менее общим.

Итак, наконец, возвращаемый тип parseподпрограмма является результатом объединения трех приведенных выше выражений и ограничения пользователя. Типresult это самый маленький тип, так как вы ограничили expressionфункция здесь, чтобы вернуть ошибки не-расширяемой наземного типа parse_error.

Теперь о смягчении.

Самое простое решение - вообще удалить аннотации типов и полагаться при программировании на средство проверки типов, мерлин и четко определенные интерфейсы (подписи). Действительно, аннотация типа здесь только смутила. Вы написали расширяемый[> ...] аннотации типа и полагал, что предполагаемый тип является расширяемым, что не соответствовало действительности.

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

| [], result -> (result : parse_error :> [> parse_error])

Если вы решите сделать свой parse_error тип расширяемый, вы не можете просто сказать

type parse_error = [> `ParseError of string]

поскольку теперь parse_error обозначает целое семейство типов, поэтому нам нужно представить эту изменчивость типа с помощью переменной типа, здесь применимы два синтаксиса,

type 'a parse_error = [>
  | `ParseError of string
  | `MoonPhaseError of int
] as 'a

или более подробный, но на мой вкус точнее,

type 'a parse_error = 'a constraint 'a = [>
    | `ParseError of string
    | `MoonPhaseError of int
  ]

Оба определения эквивалентны. Все означают этот тип'a parser_error это переменная типа 'a ул 'a включает ParseError, MoonPhaseError и бесконечно больше ошибок неопределенного рода.