[Перевод] Очисти код свободными монадами
От переводчика:
Это вольный перевод статьи «Purify code using free monads» Габриэля Гонзалеса, посвященный использованию свободных монад для представления кода как синтаксического дерева с последующей управляемой интерпретацией.
На хабре имеются другие статьи Габриэля — «Кооперативные потоки с нуля в 33 строках на Хаскеле» и «Чем хороши свободные монады».
Все замечания переводчика выделены курсивом.
По всем замечаниям, связанным с переводом, обращайтесь в личку.
Опытные программисты на Хаскеле часто советуют новичкам делать программы настолько чистыми, насколько это возможно. Функция называется чистой, если она детерминированная (возвращаемое значение однозначно определяется значениями всех формальных аргументов) и не имеет побочных эффектов (то есть не изменяет состояние среды исполнения). В классической математике, λ-исчислении и комбинаторной логике все функции чистые. Чистота предоставляет множество практических преимуществ:
- можно формально доказать какие-то свойства написанного кода,
- кроме того, можно легко обозревать код и сказать, что он делает,
- наконец, можно прогнать через QuickCheck.
Для демонстрации я буду использовать такую простенькую программу echo:
import System.Exit
main = do x <- getLine
putStrLn x
exitSuccess
putStrLn "Finished"
В приведённой программе, однако, имеется один недостаток: в ней смешаны бизнес-логика и побочные эффекты. В конкретном случае в этом нет ничего плохого, я всегда так пишу простенькие программы, которые могу целиком держать в голове. Впрочем, я надеюсь вас заинтересовать прикольными штуками, которые получаются, когда побочные эффекты отделены от бизнес-логики.
Для начала, мы должны очистить нашу программу. Отделить нечистые участки от любого кода мы можем всегда с помощью свободных монад. Свободные монады позволяют разделить любую нечистую программу на чистое представление её поведения и минимальный нечистый интерпретатор:
import Control.Monad.Free
import System.Exit hiding (ExitSuccess)
data TeletypeF x
= PutStrLn String x
| GetLine (String -> x)
| ExitSuccess
instance Functor TeletypeF where
fmap f (PutStrLn str x) = PutStrLn str (f x)
fmap f (GetLine k) = GetLine (f . k)
fmap f ExitSuccess = ExitSuccess
type Teletype = Free TeletypeF
putStrLn' :: String -> Teletype ()
putStrLn' str = liftF $ PutStrLn str ()
getLine' :: Teletype String
getLine' = liftF $ GetLine id
exitSuccess' :: Teletype r
exitSuccess' = liftF ExitSuccess
run :: Teletype r -> IO r
run (Pure r) = return r
run (Free (PutStrLn str t)) = putStrLn str >> run t
run (Free (GetLine f )) = getLine >>= run . f
run (Free ExitSuccess ) = exitSuccess
echo :: Teletype ()
echo = do str <- getLine'
putStrLn' str
exitSuccess'
putStrLn' "Finished"
main = run echo
Переписанный таким образом код собирает все нечистые действия в функции run. Я предпочитаю называть этот процесс «очищением кода», потому что мы очищаем всю логику программы до чистого кода, оставляя в стороне минимальный нечистый остаток только в нашем интерпретаторе run.
Кажется, мы не больно-то много выиграли от такого очищения кода, а заплатили за это удовольствие множеством строк кода (а ещё накладными расходами памяти и времени). Тем не менее, теперь мы можем доказать некоторые свойства нашего кода используя эквациональный вывод (equational reasoning — вывод через эквивалентные преобразования).
Например, всякий, читающий это, наверняка заметил очевидный баг в исходной программе echo:
import System.Exit
main = do x <- getLine
putStrLn x
exitSuccess
putStrLn "Finished" -- ой-ой!
Последняя команда никогда не будет исполнена… или всё же будет? Как бы это доказать?
Вообще-то мы не можем доказать, что последняя команда никогда не будет выполнена, потому что это не так. Автор модуля System.Exit мог бы запросто изменить определение exitSuccess на
exitSuccess :: IO ()
exitSuccess = return ()
Эта программа по-прежнему проходит проверку типов, но теперь она также успешно печатает Finished в консоль.
А вот для нашей очищенной версии мы можем доказать, что любая команда после exitSuccess' никогда не будет исполнена:
exitSuccess' >> m = exitSuccess'
Докажем эквациональным выводом, этим наиболее значимым профитом очищения. Эквациональный вывод предполагает, что мы можем взять любое выражение и просто подставить в определения функций компонент. Каждый шаг нижеследующего доказательства сопровождается комментарием, который указывает на конкретное функциональное определение, использованное для перехода к следующему шагу…
exitSuccess' >> m
-- exitSuccess' = liftF ExitSuccess
= liftF ExitSuccess >> m
-- m >> m' = m >>= \_ -> m'
= liftF ExitSuccess >>= \_ -> m
-- liftF f = Free (fmap Pure f)
= Free (fmap Pure ExitSuccess) >>= \_ -> m
-- fmap f ExitSuccess = ExitSuccess
= Free ExitSuccess >>= \_ -> m
-- Free m >>= f = Free (fmap (>>= f) m)
= Free (fmap (>>= \_ -> m) ExitSuccess)
-- fmap f ExitSuccess = ExitSuccess
= Free ExitSuccess
-- fmap f ExitSuccess = ExitSuccess
= Free (fmap Pure ExitSuccess)
-- liftF f = Free (fmap Pure f)
= liftF ExitSuccess
-- exitSuccess' = liftF ExitSuccess
= exitSuccess'
Обратите внимание, как на последних шагах мы перевернули равенства и перешли назад от функционального определения (справа) к определяемому выражению (слева). Такой приём полностью допустим, поскольку, благодаря чистоте, знак равенства в Хаскелле не означает присваивание, а означает действительно равенство! Это значит, что, рассуждая о коде в терминах равенства, мы можем переводить выражения в обе стороны относительно знака равенства. Впечатляет!
На самом деле равенство в Хаскеле значит не совсем равенство в традиционном понимании. В λ-исчислении есть понятие редукции — преобразования терма по определённому правилу. Формально говоря, это просто бинарное отношение на множестве термов. Терм может редуцироваться до нескольких разных термов, и эта неоднозначность обуславливает множественность стратегий редукций (энергичная — сначала редуцируется аргумент, потом выражение; ленивая — сначала всё выражение, затем аргумент по необходимости; и тому подобные). При фиксированной стратегии редукции терм либо редуцируется определённым образом до другого терма, или не редуцируется вообще никак. Последний случай называется нормальной формой терма, нами мыслится как полностью завершенное вычисление. Сами редукции порождаются какими-то правилами. Наиболее известны β- и η-редукции. В определённом смысле каждое функциональное равенство (определения функций) выражают такие же правила. Когда происходит вычисление, эти правила работают в одну сторону. Если правило замыкается на себя, происходит бесконечная рекурсия, вроде inf = inf :: a. Тем не менее, в метатеории мы можем взять это бинарное отношение и замкнуть по транзитивности и симметричности, получив бинарное отношение редукционного равенства. По теореме Черча—Россера редукционное равенство M=N справедливо тогда и только тогда, когда найдётся терм (не обязательно в нормальной форме) P такой, что оба терма M и N за какое-то конечное количество шагов редуцируются до общего значения P. Вот как раз о таких равенствах идёт речь в этой статье.
В равной степени важно и то, что вышеприведённое доказательство справедливо, как бы эта свободная монада не интерпретировалась. Мы можем поменять функцию run на любой другой интерпретатор, в т.ч. чистый, а равенство по-прежнему выполняется
exitSuccess' >> m = exitSuccess'
Это означает, что мы можем безопасно использовать его как правило переопределения в GHC (GHC rewrite rule) для оптимизации прохода по нашей программе:
{-# RULES
"exit" forall m. exitSuccess' >> m = exitSuccess'
#-}
…и мы можем гарантировать, что правило будет всегда безопасно применено и никогда не будет нарушено.
Хотелось бы доказать, что наша программа всегда выводит ту же строку, которую она получает на входе. К сожалению, это мы также не можем доказать, потому что это не так. Автор (the maintainer) функции putStrLn мог бы в любой момент передумать и переопределить
putStrLn str = return () -- худший автор в мире!
На самом деле, мы не можем даже доказать, что для очищенной свободной монадой версии это выполняется. Функция run использует тот же putStrLn, поэтому программа в любом случае подвержена той же угрозе бага. Тем не менее, мы всё же можем доказать кое-что о самой свободное монаде, рассматривая её через чистый интерпретатор:
runPure :: Teletype r -> [String] -> [String]
runPure (Pure r) xs = []
runPure (Free (PutStrLn y t)) xs = y:runPure t xs
runPure (Free (GetLine k)) [] = []
runPure (Free (GetLine k)) (x:xs) = runPure (k x) xs
runPure (Free ExitSuccess ) xs = []
Теперь мы можем доказать
runPure echo = take 1
используя функцию take из пакета Prelude стандарта Haskell98. Оставляю это в качестве упражнения для читателя, поскольку этот пост уже достаточно длинный.
Обратим внимание на ещё один важный момент. Исследуя echo сквозь призму чистого кода, мы обнаруживаем маленькую деталь, которую исходно не видели: пользователь может ничего не ввести! В этом случае наш (последний) интерпретатор должен возвратить пустой список, как и функция take _ [] = []. Эквациональный вывод принуждает нас к строгости тогда, когда простого высказывания «наша программа всегда выдаёт ту же строку, которую она получает» не достаточно. Чем больше вы работаете с подобными равенствами, тем больше совершенствуете навык рассуждения о свойствах вашего кода и обнаруживаете ошибки в ваших исходных допущениях.
В равной степени важно и то, что эквивалентные преобразования позволяют видеть вашу программу в совершенно новом свете. Мы увидели, что наша программа стала пресловутым take 1 после пропускания через runPure, что значит то, что мы можем заимствовать нашу интуицию о функции take для понимания нашей программы и обнаружения таких коварных мелких багов.
После того, как мы выделили чистую часть кода монадой Free и доказали его состоятельность, он становится надёжным ядром и нам осталось только составить интерпретатор с этого момента. Так образом, пока мы не можем полностью доказать корретность всей программы, мы могли бы доказать корректность всего, за исключением интерпретатора. В той же мере важно и то обстоятельство, что мы свели интерпретатор к абсолютно минимально подверженному для атак виду, что возволяет нам держать его в голове и поддерживать вручную.
Мы не можем ничего доказать о коде, погруженном в монаду IO. А как бы это можно было сделать? Можно было б сказать как-то то: «если скомпилировать код, запустить программу и ввести какую-то одну строку, эта же строка будет возвращена обратно», но это на самом деле не уравнение, поэтому ничего строгого в такой фразе нет. Однако, мы можем записать её как тест к нашей программе.
К сожалению, тесты нечистого кода не масштабируются на большие и сложные программы и в тестово-зависимых ЯП написание таких тестов занимает значительную долю времени всего цикла программирования.
К счастью, мы всё же можем легко испытывать чистый код при помощи библиотеки QuickCheck, которая перебирает чистые утверждения и проверяет их на некорректность в полностью автоматическом режиме.
Например, положим, что вы были слишком ленивы, чтобы доказывать runPure echo = take 1. Мы можем вместо этого попросить QuickCheck протестировать это суждение за нас:
>>> import Test.QuickCheck
>>> quickCheck (\xs -> runPure echo xs == take 1 xs)
+++ OK, passed 100 tests.
Круто! Вы можете тестировать ваш код намного активнее, если он настолько чист, насколько возможно.
Эквациональный вывод работает только для чистого кода, так что чистые участки кода служат достоверным ядром, который вы можете:
- проверить на правильность, целостность и корректность (prove soundness),
- вывести свойства его поведения (reason about behavior),
- активно тестировать (aggressively test).
Вот почему мы всегда боремся за долю чистого кода в нашем коде и сводим к минимуму нечистые части.
К счастью, свободная монада Free гарантирует нам легкое достижение высокого уровня чистоты, насколько это возможно, и наимешнего количества нечистого кода. Вот почему все опытные программисты-хаскеллисты должны свободно владеть свободными монадами.
Спасибо KolodeznyDiver за помощь в переводе.
