Spec-Zone.ru › OCaml
☰Язык OCaml
  • Язык OCaml
  • Расширения языка

Глава 12. Расширения языка

24 Обработчики эффектов

  • 24.1 Основы
  • 24.2 Параллелизм
  • 24.3 Потоки пользовательского уровня
  • 24.4 Инверсия управления
  • 24.5 Семантика
  • 24.6 Поверхностные обработчики

(Добавлено в версии 5.0. Поддержка синтаксиса для глубоких обработчиков добавлена в версии 5.3.)

pattern ::= ...
∣ effect pattern, value-name

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

24.1 Основы

Для начала определим эффект (то есть операцию), которая принимает целочисленный аргумент и возвращает целочисленный результат. Назовём этот эффект Xchg.

open Effect
open Effect.Deep

type _ Effect.t += Xchg: int -> int t
let comp1 () = perform (Xchg 0) + perform (Xchg 1)

Мы объявляем эффект обмена Xchg, расширяя предопределённый расширяемый вариантный тип Effect.t новым конструктором Xchg: int -> int t. Интуитивно это объявление можно прочитать так: «эффект Xchg принимает целочисленный параметр, а при выполнении этого эффекта возвращает целое число». Вычисление comp1 дважды выполняет эффект с помощью примитива perform и возвращает сумму результатов.

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

try comp1 () with
| effect (Xchg n), k -> continue k (n+1)

- : int = 3

Мы запускаем вычисление comp1 () под обработчиком эффекта, который обрабатывает эффект Xchg, связывая продолжение с именем k. Здесь effect — это ключевое слово, указывающее, что шаблон Xchg n сопоставляется с эффектами, а не с исключениями. Как упоминалось выше, обработчики эффектов обобщают обработчики исключений. Подобно обработчикам исключений, когда вычисление выполняет эффект Xchg, управление передаётся соответствующему обработчику, а необработанные эффекты передаются внешнему обработчику. Однако, в отличие от обработчиков исключений, обработчик также получает ограниченное продолжение k, представляющее приостановленное вычисление между точкой вызова perform и этим обработчиком.

Обработчик использует примитив continue, чтобы возобновить приостановленное вычисление со значением, следующим за предложенным. В этом примере вычисление comp1 выполняет эффекты Xchg 0 и Xchg 1 и получает от обработчика значения 1 и 2 соответственно. Поэтому всё выражение вычисляется в 3.

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

24.2 Параллелизм

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

Задача либо приостановлена, либо завершена. Представим состояние задачи следующим образом:

type 'a status =
  Complete of 'a
| Suspended of {msg: int; cont: (int, 'a status) continuation}

Задача либо завершена с результатом типа 'a, либо приостановлена: в этом случае у неё есть сообщение msg, которое нужно отправить, и продолжение cont. Тип (int,'a status) continuation означает, что приостановленное ограниченное вычисление ожидает значение типа int для возобновления и после возобновления возвращает значение типа 'a status.

Далее определим функцию step, которая выполняет один шаг вычисления, пока оно не завершится или не приостановится:

let step (f : unit -> 'a) () : 'a status =
  match f () with
  | v -> Complete v
  | effect (Xchg msg), cont -> Suspended {msg; cont}

Аргумент функции step, f, — это вычисление, которое может выполнить эффект Xchg и возвращает результат типа 'a. Сама функция step возвращает значение типа 'a status. Подобно шаблонам исключений в выражении match ... with (11.6), OCaml также поддерживает шаблоны effect. Здесь мы сопоставляем с шаблоном результат выполнения вычисления f. Если вычисление возвращает значение v, мы возвращаем Complete v. Если же вычисление выполняет эффект Xchg msg с продолжением cont, мы возвращаем Suspended {msg;cont}. В этом случае обработчик не вызывает продолжение cont сразу, а сохраняет его в структуре данных для последующего использования.

Поскольку функция step обрабатывает эффект Xchg, вычисление step f этот эффект не выполняет. Однако оно может выполнять другие эффекты. Кроме того, поскольку мы используем глубокие обработчики, сохранённое в состоянии продолжение cont также не выполняет эффект Xchg.

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

let rec run_both a b =
  match a (), b () with
  | Complete va, Complete vb -> (va, vb)
  | Suspended {msg = m1; cont = k1},
    Suspended {msg = m2; cont = k2} ->
      run_both (fun () -> continue k1 m2)
               (fun () -> continue k2 m1)
  | _ -> failwith "Improper synchronization"

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

Теперь можно определить второе вычисление, которое также обменивается двумя сообщениями:

let comp2 () = perform (Xchg 21) * perform (Xchg 21)

Наконец, можно запустить оба вычисления вместе:

run_both (step comp1) (step comp2)

- : int * int = (42, 0)

Вычисление comp1 предлагает значения 0 и 1, а в обмен получает значения 21 и 21, которые складывает, получая 42. Вычисление comp2 предлагает значения 21 и 21, а в обмен получает значения 0 и 1, которые перемножает, получая 0. Взаимодействие между двумя вычислениями целиком реализовано внутри run_both. Действительно, сами по себе определения comp1 и comp2 не задают никакого смысла эффекта Xchg.

24.3 Потоки пользовательского уровня

Расширим предыдущий пример на произвольное число задач. Многие языки, такие как GHC Haskell и Go, предоставляют потоки пользовательского уровня как примитивную возможность, реализованную в среде выполнения. С помощью обработчиков эффектов потоки пользовательского уровня и их планировщики можно реализовать непосредственно на OCaml. Обычно системы потоков пользовательского уровня предоставляют примитив fork для создания новой параллельной задачи и примитив yield для передачи управления другой задаче. Соответственно, объявим два эффекта:

type _ Effect.t += Fork : (unit -> unit) -> unit t
                 | Yield : unit t

Эффект Fork принимает функцию без аргументов (отложенное вычисление, представленное функцией типа unit -> unit) и возвращает единичное значение тому, кто его выполняет. Эффект Yield не имеет параметров и при выполнении возвращает единичное значение. Будем считать, что эффект Xchg, выполняемый задачей, может сопоставляться с эффектом обмена, выполняемым любой другой задачей, которая также предлагает обменять значение.

Также определим вспомогательные функции, которые просто выполняют эти эффекты:

let fork f = perform (Fork f)
let yield () = perform Yield
let xchg v = perform (Xchg v)

Функция верхнего уровня run задаёт планировщик:

(* A concurrent round-robin scheduler *)
let run (main : unit -> unit) : unit =
  let exchanger : (int * (int, unit) continuation) option ref =
    ref None (* waiting exchanger *)
  in
  let run_q = Queue.create () in (* scheduler queue *)
  let enqueue k v =
    let task () = continue k v in
    Queue.push task run_q
  in
  let dequeue () =
    if Queue.is_empty run_q then () (* done *)
    else begin
      let task = Queue.pop run_q in
      task ()
    end
  in
  let rec spawn (f : unit -> unit) : unit =
    match f () with
    | () -> dequeue ()
    | exception e ->
        print_endline (Printexc.to_string e);
        dequeue ()
    | effect Yield, k -> enqueue k (); dequeue ()
    | effect (Fork f), k -> enqueue k (); spawn f
    | effect (Xchg n), k ->
        begin match !exchanger with
        | Some (n', k') -> exchanger := None; enqueue k' n; continue k n'
        | None -> exchanger := Some (n, k); dequeue ()
        end
  in
  spawn main

Для хранения очереди планировщика мы используем изменяемую очередь run_q. Очередь FIFO обеспечивает циклическое планирование задач. Функция enqueue помещает задачи в очередь, а dequeue извлекает задачи из очереди и запускает их. Ячейка-ссылка exchanger хранит (приостановленную) задачу, предлагающую обменять значение. В любой момент времени может быть ноль или одна приостановленная задача, ожидающая обмена.

Основную работу выполняет функция spawn. Она запускает заданное вычисление f под обработчиком эффекта. Если f возвращает единичное значение, функция извлекает из очереди планировщика следующую задачу и запускает её. Если вычисление f возбуждает исключение, функция выводит его в стандартный поток вывода и запускает следующую задачу планировщика.

Вычисление f также может выполнять эффекты. Если f выполняет эффект Yield, текущая задача приостанавливается (добавляется в очередь готовых задач), а затем запускается следующая задача из очереди планировщика. Если выполняется эффект Fork f, текущая задача приостанавливается, а новая задача f запускается немедленно посредством хвостового вызова spawn f. Заметьте, что выбор в пользу немедленного запуска новой задачи произволен. Вместо этого мы вполне могли бы поместить задачу f в очередь готовых задач и сразу возобновить k.

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

Теперь можно написать параллельную программу, использующую только что определённые операции:

open Printf

let _ = run (fun _ ->
  fork (fun _ ->
    printf "[t1] Sending 0\n";
    let v = xchg 0 in
    printf "[t1] received %d\n" v);
  fork (fun _ ->
    printf "[t2] Sending 1\n";
    let v = xchg 1 in
    printf "[t2] received %d\n" v))

[t1] Sending 0
[t2] Sending 1
[t2] received 0
[t1] received 1

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

Возобновление с исключением

Помимо возобновления продолжения со значением, обработчики эффектов позволяют возобновить его, возбудив исключение в точке выполнения эффекта. Для этого служит примитив discontinue. Он помогает гарантировать, что ресурсы в конечном итоге всегда будут освобождены, даже при наличии эффектов.

Например, рассмотрим операцию извлечения из очереди из предыдущего примера, приведённую ниже:

…
let dequeue () =
  if Queue.is_empty run_q then () (* done *)
  else (Queue.pop run_q) ()

Если очередь планировщика пуста, функция dequeue считает, что работа планировщика завершена, и возвращает управление вызывающему коду. Однако всё ещё может оставаться задача, ожидающая обмена значением (сохранённая в ячейке-ссылке exchanger), которая навсегда останется заблокированной! Если заблокированная задача удерживает ресурсы, произойдёт утечка этих ресурсов. Например, рассмотрим следующую задачу:

let leaky_task () =
  fork (fun _ ->
    let oc = open_out "secret.txt" in
    Fun.protect ~finally:(fun _ -> close_out oc) (fun _ ->
      output_value oc (xchg 0)))

Задача записывает полученное сообщение в файл secret.txt. Она использует Fun.protect, чтобы гарантировать закрытие выходного канала oc как при обычном завершении, так и при исключении. К сожалению, этого недостаточно. Если эффект обмена xchg 0 не удаётся сопоставить с эффектом обмена, выполненным каким-либо другим потоком, эта задача навсегда остаётся заблокированной. Таким образом, выходной канал oc никогда не будет закрыт.

Чтобы избежать этой проблемы, нужно следовать простому правилу: каждое продолжение в конечном итоге должно быть либо возобновлено, либо прервано. Здесь мы используем discontinue, чтобы заблокированная задача не оставалась заблокированной навсегда. Прерывая эту задачу, мы заставляем её завершиться (с исключением):

exception Improper_synchronization

let dequeue () =
  if Queue.is_empty run_q then begin
    match !exchanger with
    | None -> () (* done *)
    | Some (n, k) ->
        exchanger := None;
        discontinue k Improper_synchronization
  end else (Queue.pop run_q) ()

Когда очередь планировщика пуста, а поток-обменщик заблокирован, функция dequeue прерывает заблокированный поток, возбуждая исключение Improper_synchronization. Это исключение возникает при заблокированном вызове функции xchg, в результате чего выполняется блок finally и закрывается выходной канал oc. С точки зрения пользователя, вызов функции xchg 0 возбуждает исключение Improper_synchronization.

24.4 Инверсия управления

При обходе структуры данных существует два основных подхода, различающихся тем, кто управляет обходом: производитель или потребитель. Например, в List.iter f l управление принадлежит производителю List.iter, который передаёт элементы потребителю f для обработки. С другой стороны, модуль Seq предоставляет механизм, похожий на отложенные списки, в котором обходом управляет потребитель. Например, Seq.forever Random.bool возвращает бесконечную последовательность случайных битов, каждый из которых создаётся (по запросу) по требованию потребителя.

Естественно, производители вроде List.iter проще пишутся в первом стиле. Второй стиль удобнее для потребителя, поскольку предпочтительнее и естественнее самому управлять процессом. Чтобы объединить преимущества обоих подходов, хотелось бы писать производителя в первом стиле и автоматически преобразовывать его во второй. Благодаря обработчикам эффектов это преобразование можно реализовать один раз и навсегда в виде библиотечной функции. Назовём эту функцию invert. Сначала рассмотрим, как использовать функцию invert, а затем — подробности её реализации. Ниже указан тип этой функции:

val invert : iter:(('a -> unit) -> unit) -> 'a Seq.t

Функция invert принимает функцию iter (производителя, который передаёт элементы потребителю) и возвращает последовательность (в которой управляет потребитель). Например:

let lst_iter = Fun.flip List.iter [1;2;3]

val lst_iter : (int -> unit) -> unit = 

— это функция iter с типом (int -> unit) -> unit. Выражение lst_iter f передаёт элементы 1, 2 и 3 потребителю f. Например:

lst_iter (fun i -> Printf.printf "%d\n" i)

1
2
3
- : unit = ()

Выражение invert lst_iter возвращает последовательность, позволяющую потребителю обходить список по запросу. Например:

let s = invert ~iter:lst_iter
let next = Seq.to_dispenser s;;

val s : int Seq.t = 
val next : unit -> int option = 
next();;

- : int option = Some 1
next();;

- : int option = Some 2
next();;

- : int option = Some 3
next();;

- : int option = None

Эту же функцию invert можно использовать с любой функцией iter. Например:

let s = invert ~iter:(Fun.flip String.iter "OCaml")
let next = Seq.to_dispenser s;;

val s : char Seq.t = 
val next : unit -> char option = 
next();;

- : char option = Some 'O'
next();;

- : char option = Some 'C'
next();;

- : char option = Some 'a'
next();;

- : char option = Some 'm'
next();;

- : char option = Some 'l'
next();;

- : char option = None

Реализация инверсии управления

Ниже приведена реализация функции invert:

let invert (type a) ~(iter : (a -> unit) -> unit) : a Seq.t =
  let module M = struct
    type _ Effect.t += Yield : a -> unit t
  end in
  let yield v = perform (M.Yield v) in
  fun () -> match iter yield with
  | () -> Seq.Nil
  | effect M.Yield v, k -> Seq.Cons (v, continue k)

Функция invert объявляет эффект Yield, принимающий в качестве параметра выдаваемый элемент. Функция yield выполняет эффект Yield. Лямбда-абстракция fun () -> ... откладывает все действия до момента, когда будет запрошен первый элемент последовательности. После этого вычисление iter yield выполняется под обработчиком эффекта. Каждый раз, когда функция iter передаёт элемент функции yield, вычисление прерывается эффектом Yield. Эффект Yield обрабатывается возвратом значения Seq.Cons(v,continue k) потребителю. Потребитель получает элемент v и приостановленное вычисление, которое с его точки зрения является просто хвостом последовательности.

Когда потребитель запрашивает следующий элемент последовательности (применяя к ней ()), продолжение k возобновляется. Это позволяет вычислению iter yield продолжить работу, пока оно не выдаст следующий элемент или не завершится обычным образом. В последнем случае возвращается значение Seq.Nil, указывающее потребителю на завершение обхода.

Важно отметить, что последовательность, возвращаемая функцией invert, является одноразовой (в терминологии модуля Seq): её можно использовать не более одного раза. Кроме того, последовательность необходимо полностью потребить (то есть использовать хотя бы один раз), чтобы гарантировать линейное использование захваченного продолжения.

24.5 Семантика

В этом разделе мы рассмотрим семантику обработчиков эффектов на примерах.

Вложенные обработчики

Как и обработчики исключений, обработчики эффектов могут быть вложенными.

type _ Effect.t += E : int t
                 | F : string t

let foo () = perform F

let bar () =
  try foo () with
  | effect E, k -> failwith "impossible"

let baz () =
  try bar () with
  | effect F, k -> continue k "Hello, world!"

В этом примере вычисление foo выполняет эффект F, внутренний обработчик обрабатывает только E, а внешний — F. Вызов baz возвращает Hello, world!.

baz ()

- : string = "Hello, world!"

Файберы

Чтобы оценить принятые проектные решения и характеристики производительности, полезно немного знать о реализации обработчиков эффектов. Обработчики эффектов реализованы с помощью управляемых средой выполнения динамически растущих сегментов стека, называемых файберами. Стек программы в OCaml представляет собой связный список таких файберов.

Для вычисления фрагмента, заключённого в обработчик эффекта, выделяется новый файбер. Файбер освобождается, когда вычисление возвращается к вызывающему коду — обычным образом, вернув значение, либо возбудив исключение.

В точке вызова perform в функции foo из предыдущего примера стек программы выглядит так:

+-----+   +-----+   +-----+
|     |   |     |   |     |
| baz |<--| bar |<--| foo |
|     |   |     |   |     |
|     |   |     |   |     |
+-----+   +-----+   +-----+ <- stack_pointer

Эти две связи соответствуют двум обработчикам эффектов в программе. Когда эффект F обрабатывается в baz, состояние программы выглядит следующим образом:

+-----+                   +-----+   +-----+
|     |                   |     |   |     |   +-+
| baz |                   | bar |<--| foo |<--|k|
|     |                   |     |   |     |   +-+
+-----+ <- stack_pointer  +-----+   +-----+

Ограниченное продолжение k — это объект в куче, который ссылается на сегмент стека, соответствующий приостановленному вычислению. Захват продолжения не требует копирования кадров стека. При возобновлении продолжения стек восстанавливается до прежнего состояния: сегмент, на который указывает k, связывается с текущим стеком. Поскольку ни захват продолжения, ни его возобновление не требуют копирования кадров стека, приостановка выполнения с помощью perform и его возобновление с помощью continue или discontinue выполняются быстро.

Необработанные эффекты

В отличие от языков Eff и Koka, обработчики эффектов в OCaml не обеспечивают безопасность эффектов: компилятор не проверяет статически, что все эффекты, выполняемые программой, обработаны. Если для эффекта нет соответствующего обработчика, в точке соответствующего вызова perform возбуждается исключение Effect.Unhandled. Например, в предыдущем примере функция bar не обрабатывает эффект F. Поэтому при запуске bar будет возбуждено исключение Effect.Unhandled F.

try bar () with Effect.Unhandled F -> "Saw Effect.Unhandled exception"

- : string = "Saw Effect.Unhandled exception"

Линейные продолжения

Как обсуждалось ранее 12.24.3, ограниченные продолжения в OCaml должны использоваться линейно — каждое захваченное продолжение необходимо возобновить ровно один раз с помощью continue или discontinue. Попытка использовать продолжение более одного раза приводит к исключению Continuation_already_resumed. Например:

try perform (Xchg 0) with
| effect Xchg n, k -> continue k 21 + continue k 21

Exception: Stdlib.Effect.Continuation_already_resumed.

Главная причина добавления обработчиков эффектов в OCaml — поддержка параллельного программирования. Однократных продолжений достаточно почти для всех задач параллельного программирования. Кроме того, их реализация обходится значительно дешевле, чем реализация многократных продолжений, поскольку не требует копирования стековых кадров. Более того, программы на OCaml могут работать с линейными ресурсами, такими как сокеты и файловые дескрипторы. Если разрешить возобновлять продолжения более одного раза, дисциплина линейности легко нарушается. Такие нарушения линейности ресурсов было бы довольно сложно отлаживать из-за отсутствия статических проверок линейности и нелокального характера потока управления. Поэтому OCaml не поддерживает многократные продолжения.

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

Чтобы гарантировать освобождение ресурсов, для захваченного продолжения можно установить финализатор:

exception Unwind
Gc.finalise (fun k ->
  try ignore (discontinue k Unwind) with _ -> ()) k

В этом случае, если k становится недостижимым, финализатор гарантирует разматывание стека продолжения, прерывая его исключением Unwind, что позволяет вычислению освободить ресурсы. Однако затраты времени выполнения на финализаторы намного выше, чем на захват продолжения. Поэтому рекомендуется возобновлять продолжение ровно один раз, а не полагаться на финализатор.

Ограничения

Эффекты OCaml являются синхронными: выполнить эффект асинхронно из обработчика сигнала, финализатора, обратного вызова memprof или сигнала тревоги GC и перехватить его в основной части кода невозможно. Вместо этого будет вызвано исключение Effect.Unhandled (12.24.5).

Аналогично, эффекты несовместимы с использованием обратных вызовов из C в OCaml (раздел 23.7). Эффект не может пересечь вызов caml_callback; вместо этого будет вызвано исключение Effect.Unhandled. В частности, при совместном использовании библиотек, в которых применяются обратные вызовы из C в OCaml, и библиотек, использующих эффекты, необходимо соблюдать осторожность.

24.6 Поверхностные обработчики

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

В OCaml также есть поверхностные обработчики. В отличие от глубоких, поверхностный обработчик обрабатывает только первый эффект, выполняемый вычислением. Продолжение, захваченное в поверхностном обработчике, не включает обработчик. Это означает, что при возобновлении продолжения обработчик уже отсутствует. Поэтому при возобновлении продолжения пользователь должен предоставить новый обработчик эффектов (возможно, другой), чтобы обработать следующий эффект, который может выполнить вычисление.

Поверхностные обработчики упрощают выражение некоторых видов программ. Реализуем поверхностный обработчик, который обеспечивает соблюдение заданной последовательности эффектов (протокола) при вычислении. В этом примере предположим, что вычисление может выполнять следующие эффекты:

type _ Effect.t += Send : int -> unit Effect.t
                 | Recv : int Effect.t

Предположим, что мы хотим обеспечить соблюдение протокола, допускающего только чередующуюся последовательность эффектов Send и Recv, соответствующую регулярному выражению (Send;Recv)*;Send?. Таким образом, разрешены последовательности эффектов [] (пустая последовательность), [Send], [Send;Recv], [Send;Recv;Send] и т. д., но не [Recv], [Send;Send], [Send;Recv;Recv] и т. д. Здесь важно то, что набор обрабатываемых эффектов меняется со временем. Как показано ниже, с помощью поверхностных обработчиков можно естественным образом обеспечить соблюдение этого протокола:

open Effect.Shallow

let run (comp: unit -> unit) : unit =
  let rec loop_send : type a. (a,unit) continuation -> a -> unit = fun k v ->
    continue_with k v
      { retc = Fun.id;
        exnc = raise;
        effc = fun (type b) (eff : b Effect.t) ->
          match eff with
          | Send n -> Some (fun (k: (b,_) continuation) ->
              loop_recv n k ())
          | Recv -> failwith "protocol violation"
          | _ -> None }
  and loop_recv : type a. int -> (a,unit) continuation -> a -> unit = fun n k v ->
    continue_with k v
      { retc = Fun.id;
        exnc = raise;
        effc = fun (type b) (eff : b Effect.t) ->
          match eff with
          | Recv -> Some (fun (k: (b,_) continuation) ->
              loop_send k n)
          | Send v -> failwith "protocol violation"
          | _ -> None }
  in
  loop_send (fiber comp) ()

Функция run выполняет вычисление comp, гарантируя, что оно может выполнять только чередующуюся последовательность эффектов Send и Recv. В поверхностном обработчике используются другие примитивы, чем в глубоком. Примитив fiber (в последней строке) принимает функцию 'a -> 'b и возвращает ('a,'b) Effect.Shallow.continuation.

В отличие от глубоких обработчиков, для поверхностных обработчиков в OCaml не предусмотрен синтаксический сахар. Выражение continue_with k v h возобновляет продолжение k со значением v под обработчиком h. Обработчик представляет собой запись с тремя полями: для случая возврата значения (retc), случая исключения (exnc) и случая эффекта (effc).

Взаимно рекурсивные функции loop_send и loop_recv возобновляют переданное продолжение k со значением v под разными обработчиками. Функция loop_send обрабатывает эффект Send и выполняет хвостовой вызов функции loop_recv. Если вычисление выполняет эффект Recv, функция loop_send прерывает вычисление, вызывая исключение. Аналогично, функция loop_recv обрабатывает эффект Recv и выполняет хвостовой вызов функции loop_send. Если вычисление выполняет эффект Send, функция loop_recv прерывает вычисление. Поскольку продолжение, захваченное поверхностным обработчиком, не включает сам обработчик, в динамической области видимости вычисления comp всегда установлен только один обработчик.

Обратите внимание: в отличие от глубоких обработчиков с синтаксической поддержкой, для поверхностного обработчика необходимы явные аннотации типов. В обработчике эффектов (effc) необходимо использовать локально абстрактный тип (type b) и явно указать тип аргумента эффекта eff и продолжения k в каждом из случаев обработки эффектов. Также следует отметить, что необходим общий случай для всех остальных эффектов «| _ -> None». Его можно интуитивно прочитать как «передать необработанные эффекты внешнему обработчику». Стандартный библиотечный модуль Effect также предоставляет несинтаксическую версию глубоких обработчиков, для которой требуются аналогичные аннотации.

Вычисление изначально запускается функцией loop_send (см. последнюю строку приведённого выше кода), которая гарантирует, что первым эффектом, который может выполнить вычисление, будет эффект Send. Обратите внимание, что вычисление может свободно выполнять эффекты, отличные от Send и Recv; их может обработать внешний обработчик.

Как видно, функция run разрешит вычисление, соблюдающее протокол:

run (fun () ->
  printf "Send 42\n";
  perform (Send 42);
  printf "Recv: %d\n" (perform Recv);
  printf "Send 43\n";
  perform (Send 43);
  printf "Recv: %d\n" (perform Recv))

Send 42
Recv: 42
Send 43
Recv: 43
- : unit = ()

а вычисления, не соблюдающие его, прервёт:

run (fun () ->
  Printf.printf "Send 0\n";
  perform (Send 0);
  Printf.printf "Send 1\n";
  perform (Send 1) (* protocol violation *))

Send 0
Send 1
Exception: Failure "protocol violation".

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

« Операторы связыванияДизамбигуация литералов массивов с учётом типов »
Copyright © 2026 Institut National de Recherche en Informatique et en Automatique

© 1995-2026 INRIA.
https://ocaml.org/manual/5.5/effects.html

Spec-Zone.ru

Настройки Оффлайн Что нового Помощь О нас
Spec-Zone .ru
спецификации, руководства, описания, API