Суть побочных эффектов в чисто функциональных языках

Выборочный перевод статьи «The Gist of Side Effects in Pure Functional Languages».

• Функциональное программирование
• Чистота и побочные эффекты
• Монады
• Типы, гарантирующие уникальность
• Послесловие от переводчика: о ленивости

Функциональное программирование

Функциональное программирование основано на двух центральных идеях: (1) вычисления происходят путем применения функций к их аргументам и (2) функции являются объектами первого класса. В частности, функции могут передаваться или возвращаться другими функциями и могут быть компонентами структур данных. Функциональные языки различаются в зависимости от того, строго ли они проверяются по типу, слабо или вообще не проверяются нет; проверяются ли они динамически или статически; чистые они или нечистые; и, наконец, строгие они или нет.

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

Здесь мы объясняем суть того, как добиться побочных эффектов в чистых языках функционального программирования. Нашим средством для иллюстрации является функциональный язык программирования Haskell, язык со строгой типизацией, чистый и с ленивыми вычислениями, который в значительной степени является «стандартным» ленивым языком. Чистота и нестрогость — это не только вопрос стиля. Программы на нечистых, строгих языках будут выглядеть и работать совершенно иначе, чем их чистые аналоги. Основное преимущество чистоты — ссылочная прозрачность. Основными преимуществами нестрогости являются более высокая модульность и меньшая связанность с проблемами вычислений.

Чистота и побочные эффекты

Чистота не противоречит вычислениям, требующим побочных эффектов, таких как ввод-вывод, деструктивные обновления, параллелизм, исключения или языковое взаимодействие с программами, написанными на других языках программирования. Как такое возможно? Хорошо известно, что выражения в чистых функциональных языках прозрачны по ссылкам, поэтому переменные неизменяемы или постоянны — они не могут содержать разные значения в разное время. Но также хорошо известно, что вычисление с отслеживанием состояния можно «смоделировать» функционально, явно передавая состояние от функции к функции в качестве дополнительного параметра. Правда, есть механизм, который несколько сбивает с толку, называемый «потоком», потому что состояние «переплетено» от функции к функции. Термины «многопоточность» и «потоки» приобрели более конкретное значение из-за их использования в параллелизме и операционных системах, мы их не будем здесь рассматривать.

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

• Императивно. Так, пара или кортеж состоит из значения счетчика в программе и набора всех постоянных и изменяемых переменных программы вместе с их текущими значениями. Изменяемые переменные — это переменные, которые содержат разные значения в разное время выполнения посредством присваиваний. Например, в императивной программе только с двумя переменными x и y, которые претерпевают серию прямых или косвенных присваиваний во время выполнения, состояние в момент времени t будет кортеж

  < t, {<x, vx>, <y, vy>} >
  

  где v_x — значение, хранящееся в x, а v_y — значение, сохраненное в y, в момент времени t. Выполнение измеряется количеством выполненных инструкций, поэтому t — значение счетчика в программе.
• Чисто функционально. Так, последовательность неизменяемых значений состояния передаются и возвращаются от функции к функции. Возьмем, к примеру, присвоение x := w. Предположим, что присвоение происходит в момент времени t и требует k инструкций, изменение состояния можно изобразить как отображение (предположим, что v_w является значением выражения w):

  < t, {<x, vx>, <y, vy>} >  →  < t + k, { <x, vw>, <y, vy> } >
  

  Назовем состояние слева от стрелки s₀ и состояние справа от стрелки s₁. Команду присваивания можно смоделировать с помощью следующей функции

  update <x, w> s0 = s1
  

  Эта функция принимает переменную и выражение, участвующие в присвоении, плюс начальное состояние и возвращает новое состояние. В функциональной парадигме значение переменной s₀, содержащее состояние до присвоения, является неизменным, значит и значение s₁ так же неизменно.

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

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

getChar :: File → Char

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

getChar :: File → State → (Char, State)

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

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

let (c1, s1) = getChar file s0
    (c2, s2) = getChar file s0
in...

Два выражения вызова getChar совместно используют состояние s0, а второй вызов считывает символ из начального состояния, не обращая внимания на то, что символ уже был прочитан из файла.

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

g :: t0 → State → (t1, State) -- Функция g принимает значение типа t0, значение типа
			      -- State, возвращает кортеж, первый компонент которого
			      -- имеет тип t1, а второй — новое значение типа State.
f :: t1 → State → (t2, State) -- Функция f принимает значение типа t1, значение типа
			      -- State, возвращает кортеж, первый компонент которого
			      -- имеет тип t2, а второй — новое значение типа State.
compose f g v0 s0 = let (v1, s1) = g v0 s0
                        (v2, s2) = f v1 s1
                    in  (v2, s2)

Функция g принимает значение типа t0, значение типа State, и возвращает кортеж, первый компонент которого имеет тип t1, а второй компонент — новое значение типа State. Функция f принимает значение типа t1, возвращает значение типа t2, а также изменяет состояние. Как показывает код для compose, состояние должно передаваться последовательно и явно: сначала g применяется к v0 и состоянию s0, создавая значение v1 и состояние s1, а затем f применяется к v1 в состоянии s1, создавая значение v2 и состояние s2, которое является значением (кортежа), возвращаемым compose. Явная сериализация состояния не только утомительна, но и подвержена ошибкам.

Монады

Монады делают состояние неявным и скрытым, обертывая тип функций с побочными эффектами (т.е. тип функций, которые принимают состояние и возвращают значение вместе с обновленным состоянием) в абстрактный тип данных. Манипулирование состоянием происходит только с помощью двух операций: одна называется thenM, которая выстраивает в цепочку вычисления с состоянием, а другая - returnM, которая превращает значения в вычисления с сохранением состояния. Для этих операций иногда используют имена bind и return.

Точнее, функция thenM принимает три аргумента: (1) вычисление состояния, то есть выражение, в котором нечистая функция применяется к своим аргументам, но ещё не к текущему состоянию, (2) нечистая функция и (3) текущее состояние. Вычисление состояния применяется ими к текущему состоянию, производящему новое значение и новое состояние, которые, в свою очередь, передаются нечистой функции, которая дает конечный результат пары значение-состояние.

В приведенном ниже коде t в сигнатуре типа обозначает некоторый тип значений, v обозначает само значение, а s — значение состояния. Тип State — это тип значений состояния, которыми может управлять внутренняя система времени выполнения. Во многих реализациях то, что фактически передаётся как значение состояния, является указателем на глобальную переменную. Для удобства определим синоним типа,

type M t = State → (t,State)

getChar :: File → State → (Char, State)
getChar :: File → M Char

thenM :: M t0 → (t0 → M t1) → M t1
h `thenM` f = λs → let (v1, s1) = h s
                   in f v1 s1

Обратные кавычки в определении thenM — это синтаксис Haskell для написания каррированных функций с двумя аргументами в инфиксной форме. В определении h — это вычисление с сохранением состояния, которое применяется к текущему состоянию s (которое должно быть передано в качестве аргумента), а f — это нечистая функция, которая применяется к значению и состоянию, полученным применением h к s. Если текущее значение состояния s0, то:

(h `thenM` f) s0

f v1 s1

Функция returnM принимает чистое значение и возвращает функцию, которая задает состояние, возвращает это самое значение и состояние без изменений, то есть, если v является значением, приложение returnM v является вычислением с отслеживанием состояния, которое возвращает это значение, не влияя на состояние; следовательно, thenM - это греховная операция, которая позволяет нам превращать чистые ценности (которые живут в мире без состояния) в нечистые (которые живут в мире с состоянием). А если вы станете нечистым, то искупление невозможно: мы не определили операцию, которая принимает вычисление с сохранением состояния и получает значение, но игнорирует состояние. Определение returnM:

returnM :: t → M t
returnM = λv → (λs → (v, s))

С помощью этих двух операций можно составить нечистые функции. Фактически, сам состав нечистой функции можно определить следующим образом:

compose f g v0 s0 =
    ((g v0) `thenM` (λv1 → (f v1) `thenM` (λv2 → returnM v2))) s0

λv1 → (f v1) `thenM` (λv2 → returnM v2)

compose f g v0 =
    (g v0) `thenM` (λv1 → (f v1) `thenM` (λv2 → returnM v2))

Обратите внимание, что в определении не упоминаются переменные состояния! Более того, оно может выглядеть ещё более императивным, если оно написано с использованием синтаксического сахара, известного как do-нотация. Действия (вычисления) внутри do происходят последовательно.

compose f g v0 = do v1 ← g v0 -- здесь неявно `thenM`
                    v2 ← f v1 -- здесь неявно `thenM`
                    returnM v2

Состояние окончательно инкапсулируется, когда полиморфный тип M определяется как абстрактный тип данных, а не как синоним типа. В Haskell для случая ввода-вывода абстрактный тип M называется IO; следовательно:

getChar :: File → IO Char

Пример ниже показывает, как нечистая функция getString считывает строку (последовательность символов) из файла. В первом блоке (getString file = (getChar file) `thenM` ...) показана функция, записанная в терминах thenM и returnM. Второй блок (getString file = do c ← getChar file ...) представляет собой визуализацию первого блока в более удобочитаемой do-нотации, которая также является более обязывающей по стилю. Обратите внимание на использование рекурсии в обоих.

getString :: File → IO String
getString file =
  (getChar file) `thenM`
     (λc → if c == EOF then (returnM [])
                       else ((getString file) `thenM` 
                               (λs → returnM (c:s))))
getString file = do c ← getChar file
                    if c == EOF then returnM []
                                else do s ← getString file
                                     returnM (c:s)

Типы, гарантирующие уникальность

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

putChar :: Char → File → File

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

putChar :: Char → *File → *File

Состояние также скрыто, но типы с гарантией уникальности навязывают программисту некую форму сериализации и дисциплины совместного использования, который должен знать об этих ограничениях при написании программы и удостовериться, что они удовлетворяют проверке типов. Дисциплина совместного использования становится простой, когда выражения представлены непосредственно в виде графиков. Типы с гарантией уникальности связаны с линейными типами (и, следовательно, с линейной логикой из-за изоморфизма Карри-Ховарда, который идентифицирует типы с формулами в конструктивной логике и функциональные программы с доказательствами). Типы с гарантией уникальности предоставляют информацию о том, как применяется конкретная функция (линейным способом, никогда не передаётся), тогда как линейные типы предоставляют информацию о том, как выражение используется в функции.

Послесловие от переводчика: о ленивости

Ленивость — одно из важнейших качеств языков программирования, обладающий чистотой. К этому надо добавить, что ленивость так же является важнейшим качеством авторов, которые пишут статьи и книги об этих языках. Правда, эти два вида лени отличаются. Ленивые функции отрабатывают, как только возникает необходимость в их результатах. А вот ленивые авторы не отрабатывают, когда требуется разобраться в работе, которую они не доделали. Цитирую автора переведённой статьи:

функция thenM принимает три аргумента: (1) вычисление состояния, то есть выражение, в котором нечистая функция применяется к своим аргументам, но ещё не к текущему состоянию, (2) нечистая функция и (3) текущее состояние.

Обратные кавычки в определении thenM — это синтаксис Haskell для написания каррированных функций с двумя аргументами в инфиксной форме.

Разбираем первую цитату дальше. Первый аргумент — это

вычисление состояния, то есть выражение, в котором нечистая функция применяется к своим аргументам, но ещё не к текущему состоянию

нечистая функция

В подразделах «Чистота и побочные эффекты» и «Монады» автор оригинальной статьи 14 раз употребил слово «нечистая» по отношению к функциям в чистых языках программирования. Да, в рассмотренных примерах автор так и утверждает, что пишет нечистые функции. То есть в очередной раз наблюдаются «разброд и шатания»: одни пишут о поголовной чистоте функций (в том числе и монадических) в чистых языках программирования. А другие пишут о нечистых функциях в чистых языках.

P.S. Все рисунки к этой статье были выполнены переводчиком — чтобы было понятнее. А вот автор оригинальной статьи поленился это сделать.

Опубликовано: 2022.01.10, последняя правка: 2022.01.23    14:48

Добавить свой отзыв

Написать автору можно на электронную почту
mail(аt)compiler.su