Почему эта функция выравнивания для типа потока выдает мне эту ошибку?

#ocaml #type-inference

Вопрос:

 exception Empty_list

type 'a stream = Stream of 'a * (unit -> 'a stream) | Nil

let shead s = match s with
  | Stream (a, _) -> a
  | Nil -> raise Empty_list

let stail s = match s with
  | Stream (_, s) -> s ()
  | Nil -> raise Empty_list

let sflatten ( s : 'a stream ) =
  let rec sflatten_sub (s : 'b stream) parent =
    match s with
    | Nil -> parent ()
    | Stream (child, tl) ->
       match child with
       | _ -> Stream ( shead s, fun () -> sflatten_sub (tl ()) parent )
       | Stream (_, _) ->
          sflatten_sub (shead s) (fun () -> sflatten_sub (tl ()) parent)
  in sflatten_sub s (fun () -> Nil)
 

Когда я передаю это в интерпретатор ocaml (с a ;; в конце, конечно), я получаю эту ошибку, и я не понимаю, что не так.

                                           Line 21, characters 23-32:
21 |           sflatten_sub (shead s) (fun () -> sflatten_sub (tl ()) parent)
                            ^^^^^^^^^
Error: This expression has type 'a stream
       but an expression was expected of type 'a stream stream
       The type variable 'a stream occurs inside 'a stream stream
 

Ответ №1:

Вот ваши первые два рекурсивных вызова sflatten_sub :

 sflatten_sub (tl ()) parent

sflatten_sub (shead s) (fun () -> ... )
 

Первый параметр будет иметь один и тот же тип в этих двух вызовах. Поскольку tl () возвращается 'a stream , я заключаю, что shead s также возвращается 'a stream . Поскольку начало s -это поток, то s должен быть поток потоков.

Другими словами, мне кажется, что shead s это не возвращает правильный тип значения для первого параметра sflatten_sub . Он возвращает элемент потока (тип 'a ), но первым параметром sflatten_sub должен быть поток (тип 'a stream ).

Комментарии:

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

2. При параметрическом полиморфизме поведение полиморфной функции не может зависеть от типа ее полиморфного аргумента. Таким образом, невозможно (и на самом деле само понятие нечетко определено) превратить an 'a stream в a 'b stream where 'b is the non-stream part of 'a . Однако можно определить (нерегулярный) тип варианта для произвольно вложенных потоков ( type 'a nested = Final of 'a stream | Nest of 'a stream nested ).

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