Ошибки полиморфной рекурсии OCaml

Учитывая следующие виды:

type _ task =
| Success : 'a -> 'a task
| Fail : 'a -> 'a task
| Binding : (('a task -> unit) -> unit) -> 'a task
| AndThen : ('a -> 'b task) * 'a task -> 'b task
| OnError : ('a -> 'b task) * 'a task -> 'b task

type _ stack =
| NoStack : 'a stack
| AndThenStack : ('a -> 'b task) * 'b stack -> 'a stack
| OnErrorStack : ('a -> 'b task) * 'b stack -> 'a stack

type 'a process = 
{ root: 'a task 
; stack: 'a stack 
}

let rec loop : 'a. 'a process -> unit = fun proc ->
match proc.root with
| Success value -> 
    let rec step = function
    | NoStack -> ()
    | AndThenStack (callback, rest) -> loop {proc with root = callback value; stack = rest }
    | OnErrorStack (_callback, rest) -> step rest  <-- ERROR HERE
    in
    step proc.stack
| Fail value -> 
    let rec step = function
    | NoStack -> ()
    | AndThenStack (_callback, rest) -> step rest
    | OnErrorStack (callback, rest) -> loop {proc with root = callback value; stack = rest }
    in
    step proc.stack
| Binding callback -> callback (fun task -> loop {proc with root = task} )
| AndThen (callback, task) -> loop {root = task; stack = AndThenStack (callback, proc.stack)}
| OnError (callback, task) -> loop {root = task; stack = OnErrorStack (callback, proc.stack)}

Я получаю ошибку от компилятора:

Ошибка: это выражение имеет стек типа b#1, но ожидалось выражение типа 'a stack. Конструктор типа b#1 вышел бы из своей области видимости

В этой строке кода:

| Success value -> 
    let rec step = function
    | NoStack -> ()
    | AndThenStack (callback, rest) -> loop {proc with root = callback value; stack = rest }
    | OnErrorStack (_callback, rest) -> step rest  <-- ERROR HERE
    in
    step proc.stack

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

Каков правильный способ устранения этой ошибки?


ocaml gadt bucklescript
person Erik Lott    schedule 29.05.2018    source источник
comment
Обратите внимание, что сообщения об ошибках экзистенциального типа (все варианты a#987 несовместимы с b#31, это выйдет за пределы его области действия) были значительно улучшены, начиная с 4.03. Я думаю, что стоит переключиться на последний компилятор OCaml при работе с тяжелым кодом GADT.   -  person octachron    schedule 30.05.2018
comment
Это было бы большой помощью. Я новичок в GADT, и загадочные сообщения об ошибках, которые выдает OCaml v4.02.3, не помогают в обучении. К сожалению, я не могу изменить версию из-за bucklescript   -  person Erik Lott    schedule 30.05.2018

Ответы (2)


arrow_upward
0
arrow_downward

Я думаю, что есть что-то несвязное в этих функциях. Добавление некоторых аннотаций и удаление ненужных ветвей дает:

let rec loop (type s) (proc : s process) =
  match proc.root with
  | Success value -> 
      let rec step (type t) (x : t stack) =
        match x with
        | NoStack -> ()
        | AndThenStack (callback, rest) ->
            loop {proc with root = callback value; stack = rest }
                                          (*^^^^^*)
        | OnErrorStack (callback, rest) -> step rest
      in
      step proc.stack
  | _ -> ()

где "подчеркнутая" переменная является предметом сообщения об ошибке:

Ошибка: это выражение имеет тип s, но ожидалось выражение типа t

Что должно произойти, если первый проход через step работает с (OnErrorStack : unit stack), а затем второй проход через step работает с (AndThenStack : int stack)?

Другими словами, если аргумент loop выглядит примерно так:

{ root = Success ();
  stack = OnErrorStack ((fun () -> Success 3),
                        AndThenStack ((fun x -> Success (float_of_int x)),
                                      (NoStack : float stack))) }

В то время как (value : unit) будет совместимо с первым step, мне кажется, ничто не гарантирует его совместимости со вторым step, который действует скорее на значение экзистенциального типа внутри OnErrorStack (int в контрпримере).

person tbrk    schedule 29.05.2018
comment
Да, ты прав. В определении типа отсутствовало понятие, которое однажды было определено, и все было очищено. - person Erik Lott; 29.05.2018

arrow_upward
0
arrow_downward

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

type (_,_) task =
| Success : 'a -> ('a,_) task
| Fail : 'x -> (_,'x) task
| Binding : ((('a,'x) task -> unit) -> unit) -> ('a,'x) task
| AndThen : ('a -> ('b,'x) task) * ('a,'x) task -> ('b,'x) task
| OnError : ('x -> ('a,'y) task) * ('a,'x) task -> ('a,'y) task

type (_,_) stack =
| NoStack : (_,_) stack
| AndThenStack : ('a -> ('b,'x) task) * ('b,'x) stack -> ('a,'x) stack
| OnErrorStack : ('x -> ('a,'y) task) * ('a,'y) stack -> ('a,'x) stack

type ('a,'x) process = 
{ root: ('a,'x) task 
; stack: ('a,'x) stack 
}

let rec loop : type a x. (a, x) process -> unit = fun proc ->
match proc.root with
| Success value -> 
    let rec step : 'x. (a, 'x) stack -> unit = function
    | NoStack -> ()
    | AndThenStack (callback, rest) -> loop {root = callback value; stack = rest }
    | OnErrorStack (_callback, rest) -> step rest
    in
    step proc.stack
| Fail value -> 
    let rec step : 'a. ('a, x) stack -> unit = function
    | NoStack -> ()
    | AndThenStack (_callback, rest) -> step rest
    | OnErrorStack (callback, rest) -> loop {root = callback value; stack = rest }
    in
    step proc.stack
| Binding callback -> callback (fun task -> loop {proc with root = task})
| AndThen (callback, task) -> loop {root = task; stack = AndThenStack (callback, proc.stack)}
| OnError (callback, task) -> loop {root = task; stack = OnErrorStack (callback, proc.stack)}
person Erik Lott    schedule 29.05.2018