LiquidHaskell: знакомство

let author   = "Денис Шевченко"
    date     = fromGregorian 2016 dec 16
    category = "Утилиты"
    tags     = ["LiquidHaskell"]

Приветствую вас, друзья!

Сегодня мы познакомимся с удивительным инструментом, который поможет сделать наш Haskell-код ещё более надёжным и предсказуемым. Возможно, эта статья положит начало циклу публикаций, ведь русскоязычных материалов про LiquidHaskell, насколько мне известно, ешё нет. У меня была честь выступить с докладом об этом инструменте на второй fpconf. Если вы там не были - читайте.

Не всё коту масленица…

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

Рассмотрим код:

average :: Foldable t => t Int -> Int
average ns = sum ns `div` length ns

Функция average даёт нам средее значение элементов списка, складывая значения элементов и деля эту сумму на их число. Эта функция отлично справляется со своими обязанностями, но лишь до тех пор, пока мы, по злому ли умыслу или ненароком, не применим её к пустому списку:

main :: IO ()
main :: print . average $ []  -- Ой...

В этом случае функция length радостно вернёт 0, а функция div столь же радостно разделит сумму на этот самый 0…

Вот ещё пример:

checkProtocol :: [IP] -> Bool
checkProtocol = isIPv4 . head

Задумка была предельно проста: взять список IP-адресов и проверить их тип, IPv4 или IPv6. Список всегда содержал адреса одного типа, поэтому достаточно было проверить любой из них. Кроме того, список этот никогда не был пустым, поэтому разработчик обращался к первому из адресов. И вот однажды список этот - кто бы мог предположить? - оказался-таки пустым:

main :: IO ()
main :: print . checkProtocol $ []  -- И снова ой...

В этом случае функция head, как ни в чём ни бывало, попытался взять голову списка. Пустого на этот раз…

А вот моё любимое:

getUserName :: Home -> Text
getUserName homeDir = parts !! 2
  where
    parts = splitOn "/" homeDir

И снова всё просто и понятно: из полного пути к домашнему каталогу пользователя мы извлекаем его имя, разбивая путь по прямым слэшам. В результате третьим по счёту элементом списка parts и будет искомое имя. Для простоты автор этого кода отбросил экзотические случаи путей к домашнему каталогу, подразумевая лишь канонические /home/user на Linux и /Users/user на Mac. И эта функция отлично работала на этих системах, пока однажды - ну кто бы мог подумать? - её не запустили на Windows. Напомню, пути в Windows не содержат прямых слэшей, что привело к тому, что список parts не имел третьего по счёту элемента, и попытка обратиться к оному… Ну, вы поняли.

Что хуже всего, все эти примеры прекрасно компилируются. GHC не обмолвится ни единым предупреждением, и будет прав: с точки зрения языка Haskell нет никаких проблем ни в делении на ноль, ни в обращении к несуществующему элементу списка. Но мы-то с вами знаем, что проблемы есть! Просто лежат они не в области языка, а в области здравого смысла.

А вот если честно, друзья, чего бы нам по-настоящему хотелось, глядя на подобный код? Нет, не побить автора, я о другом. Нам бы хотелось, чтобы такой код не прошёл компиляцию. Как было бы здоров, правда?

Preprocessing executable 'proj' for proj-0.1.0.0...
[1 of 1] Compiling Main             ( src/Main.hs, .stack-work/dist/x86_64-linux/Cabal-1.22.5.0/build/proj/proj-tmp/Main.o )

/home/denis/proj/src/Main.hs:9:24:
    Are you a fool?! You cannot divide by zero! Go away!!

--  While building package proj-0.1.0.0 using:
      /home/denis/.stack/setup-exe-cache/x86_64-linux/Cabal-simple_mPHDZzAJ_1.22.5.0_ghc-7.10.3 --builddir=.stack-work/dist/x86_64-linux/Cabal-1.22.5.0 build exe:proj --ghc-options " -ddump-hi -ddump-to-file"
    Process exited with code: ExitFailure 1

К сожалению, наш любимый компилятор не способен на это. А значит, нам нужен инструмент, который способен.

LiquidHaskell

Когда-то группа умных людей из Калифорнийского Университета в Сан-Диего задумалась о том, что неплохо было бы усовершенствовать наши типы. Ведь что такое, по сути своей, тип? Тип - это понятное человеку обозначение множества значений. Например, сказать “Поле v имеет тип Int” - это то же самое, что сказать “Поле v на 64-разрядной платформе содержит целочисленное значение в промежутке от -9223372036854775808 до 9223372036854775807 включительно”. Тип отражает наши ожидания в отношении значения, и мы крайне признательны компилятору за его пристальное наблюдение за типами. Однако нам редко нужны столь широкие промежутки фактических значений. Например, не всякое целочисленное значение может быть отрицательным. Но типу Int всё равно, нет никаких препятствий запихнуть в него значение меньше нуля. А значит, нам нужен способ как-то уточнить наши ожидания. Так вот упомянутые люди из Калифорнийского Университета предложили делать это так:

{v : Int | v > 0}

Перед нами - тип. Да-да, вся эта конструкция задаёт новый тип, только тип хитрый. Он состоит из двух частей - базового типа и логического уточнения:

{v : Int  | v > 0      }

     Base   Refinement

Base - это обыкновенный Хаскельный тип, а Refinement - это логическое уточнение. Здесь мы как бы говорим: “Значение v будет не просто целочисленным, но обязательно положительным!” Предикат v > 0 - это и есть самое интересное, поскольку в нём отражены те наши ожидания, соответствие которым не в состоянии проверить компилятор.

Теперь введём имя для нашего нового типа:

type Positive = {v : Int | v > 0}

Так вот тип Positive - это и есть Liquid-тип. Вы спросите, откуда такое название, Liquid? Полное название звучит так: Logically Qualified Data Type, то есть Логически Уточнённый Тип Данных. Но, согласитесь, длинновато звучит. В итоге подумали создатели, подумали - и решили сделать псевдо-аббревиатуру путём выбрасывания лишних букв:

Logically Qualified Data Type

L  i      Qu    i d      Type

Прикольно, не правда ли? И запомнить легко.

Но уже слышу ваш вопрос: “И что же теперь прикажете делать с этим Positive? Ведь та странного вида конструкция с фигурными скобками не является частью языка Haskell.” Совершенно верно, не является. Эта конструкция родом из математики, она задаёт множество (а мы уже знаем, что тип и есть некое множество). И мы действительно не можем вставить этот “построитель множества” в Haskell-код, компилятор не имеет ни малейшего понятия, что делать с этим Positive. Поэтому был создан отдельный инструмент и выложен на Hackage. Этот инструмент понимает Liquid-типы и знает, что с ними делать.

Любопытно, что идея улучшать типы с помощью предикативной логики нашла своё первое воплощение не в Haskell, а в OCaml. Затем, в 2012 году, была успешно защищена докторская диссертация, темой которой была реализация Liquid-типов в Haskell, и уже в 2013 году появился пакет liquidhaskell. То есть, как видите, инструмент весьма свежий, и некоторые из Haskell-разработчиков ещё даже не слышали о нём.

Приготовимся

Ставим пакет liquidhaskell:

$ stack install liquidhaskell

Увы, он пока ещё не добавлен в Stackage-снимки, поэтому придётся расширить наш stack.yaml:

extra-deps:
- daemons-0.2.1
- located-base-0.1.1.0
- dotgen-0.4.2
- intern-0.9.1.4
- fgl-visualize-0.1.0.1
- liquid-fixpoint-0.5.0.1
- liquidhaskell-0.6.0.0

После сборки в нашем распоряжении окажется команда liquid, её-то мы и будем использовать далее.

Впрочем, если бы мы прямо сейчас запустили её, то увидели бы это:

$ liquid 
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

liquid: <no location info>: Error: Uh oh.
    LiquidHaskell requires an SMT Solver, i.e. z3, cvc4, or mathsat to be installed.

Дело в том, что мы забыли про важную штуку, без которой liquid работать не в состоянии. Нам нужен доказыватель теорем (theorem prover). Именно он поможет делать выводы о нашем коде. Ведь liquid - это статический верификатор кода, то есть инструмент, который должен делать суждения о корректности нашего кода, не запуская его. Понятное дело, что без математики тут не обойтись, потому мы и должны установить предложенный пакет:

$ sudo apt install z3

Не беспокойтесь, для других дистрибутивов он тоже есть. И в homebrew вы тоже найдёте этот пакет.

Теперь мы готовы к работе. Но прежде чем продолжать, я должен признаться: liquidhaskell пока что работает только с ghc-7.*, и если вы уже перешли на 8 версию компилятора - жаль, но вам придётся подождать новую версию верификатора. Впрочем, есть хорошая новость: авторы пакета работают над этим.

Пример с портом

Теперь выберем какой-нибудь проект и создадим новый модуль для нашей первой спецификации:

module Liquid.Spec.Port where

{-@
    type NotRootPort = {p : Int | 1024 <= p && p <= 65535}
@-}

Странный модуль, не правда ли? Кода нет, есть лишь многострочный комментарий. Этот-то комментарий нам и нужен, ведь он является спецификацией для liquid. И если для компилятора этой спецификации не существует (ибо GHC молчаливо игнорирует комментарии), то для команды liquid эта спецификация - всё, что нужно для работы.

Итак, есть в нашем приложении непривилигированные порты для Linux-системы. Тип этих портов - это не просто целое число, но такое число, которое входит в диапазон от 1024 до 65535 включительно. Этот факт и отражён в спецификации:

{p : Int | 1024 <= p && p <= 65535}

Теперь, при определении такого порта, мы пишем:

import Liquid.Spec.Port ()

{-@ localPort :: NotRootPort @-}
localPort :: Int
localPort = 3010

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

Далее мы определяем тип для localPort:

{-@ localPort :: NotRootPort @-} -- Liquid-тип
localPort :: Int                 -- Haskell-тип

Да, мы указываем тип дважды: для liquid и для компилятора. А вот теперь происходит самое интересно. Запустим верификатор:

$ stack exec -- liquid src/Main.hs

где src/Main.hs - путь к верифицируемому модулю. Понятно, что запуск в stack-контексте необходим, чтобы liquid видел импортируемые модули.

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

{-@ localPort :: NotRootPort @-}
localPort :: Int
localPort = 22  -- Ой...

результатом будет UNSAFE (с довольно-таки внушительным сообщением об ошибке), ведь значение 22 выходит за рамки наших ожиданий.

И как же работает эта магия?

Да, без магии не обошлось, если считать математику магией. Сама идея судить о корректности кода без его запуска отнюдь не новая: некоторые из соответствующих алгоритмов были сформулированы и описаны ещё в 70-х годах прошлого века (взгляните на эту публикацию). Авторы liquidhaskell решили не изобретать велосипед и взять то, что можно взять. Поэтому они соединили алгоритм Хиндли-Милнера (это тот самый механизм, который используется в Haskell для автоматического выведения типов) с предикативной логикой, получив на выходе… зависимый тип, то есть такой тип, который зависит от конкретного значения. Взгляните:

{-@ type NotRootPort = {p : Int | 1024 <= p && p <= 65535} @-}
{-@ type RootPort    = {p : Int | 0    <= p && p <  1024}  @-}

Хотя базовый тип в основе типов NotRootPort и RootPort один и тот же, эти типы воспринимаются liquid как абсолютно разные, а ведь это именно то, что нам было нужно, ведь привилигированный порт и не привилигированный - это действительно разные вещи. ;-)

Таким образом, на стадии компиляции (да-да, под капотом liquid используется ghc) выведенные типы наподобие NotRootPort сравниваются с конкретными значениями, такими как 3010, и упомянутый выше доказыватель теорем пытается разрешить (solve) соответствие или несоответствие. Так мы и получаем на выходе SAFE или UNSAFE.

Впрочем, если вы хотите больших подробностей - ознакомьтесь с прекрасной публикацией “LiquidHaskell: Experience with Refinement Types in the Real World”. Если же вы не боитесь крутой математики и желаете познать все тонкости математической магии внутри liquid - тогда вашему вниманию предложена диссертация “Liquid Types”.

Презумпция виновности

Что ж, продолжим. Определим тип для ненулевого целочисленного значения:

module Liquid.Spec.Num where

{-@
    type NotZero = {p : Int | p != 0}
@-}

Ура! Отныне нам не страшна проблема деления на ноль. Определим же функцию безопасного деления:

{-@ okDiv :: Int -> NotZero -> Int @-}
okDiv :: Int -> Int -> Int
okDiv = div

Внутри стандартная функция div, но тип делителя объявлен как ненулевой. Поэтому, если мы напишем так:

main :: IO ()
main = print $ 123 `okDiv` 0

и попытаемся верифицировать такой код, то результат будет UNSAFE.

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

main :: IO ()
main = (readLn :: IO Int) >>= print . okDiv 512

Берём из ввода то, что является целым числом (проверки для простоты опущены, пусть там действительно будет целое число) и выводим результат деления 512 на это число. И что же выдаст нам liquid? Удивлены вы или нет, выдаст он UNSAFE. Но почему? А вдруг число, полученное извне, действительно будет ненулевым? В этом-то и дело: принцип “а вдруг” тут не пройдёт. У liquid нет оснований считать, что прилетевшее извне не будет равно нулю, а значит получите UNSAFE.

Авторы liquid решили, что лучше назвать хороший код плохим, нежели плохой хорошим. Поэтому код считается небезопасным до тех пор, пока не доказана его безопасность. Из этого вытекает важный вывод: если код назван UNSAFE, он теоретически может и не быть плохим, но если уж назван SAFE - значит он сто пудов хороший!

Поэтому такой пример придётся дополнить явной проверкой:

main :: IO ()
main = (readLn :: IO Int) >>= divideIt
  where
    divideIt 0 = putStrLn "Go away!"
    divideIt v = print $ 512 `okDiv` v

Вот теперь результат будет SAFE.

Измерения

Рассмотрим ещё один пример:

servicePorts :: [Port]
servicePorts =
  [3000, 3001, 3010, 3011, 3012, 3013
   3013, 3014, 3020, 3030, 3040, 3050]

Это список портов для тестовых сервисов. И всё бы хорошо, но в список закралась досадная ошибка. Вы не видите её? Порт 3013 продублирован, а по сценарию теста порты обязаны быть уникальными. Что же делать?

Когда мы говорим об уникальности элементов, на ум приходит Set, не правда ли? Проблема в том, что если мы сконструируем из этого списка Set, повторяющееся значение 3013 будет тихо выброшено. Да, иногда это допустимо, а что если нет? Призовём на помощь liquid:

module Liquid.Spec.List where

import Data.Set

{-@ 
    type ListUnique a = {v : [a] | NoDups v}
@-}

{-@ 
    predicate NoDups L = Set_emp (dups L)
@-}

{-@
    measure dups :: [a] -> (Set a)
    dups ([])   = {v | Set_emp v}
    dups (x:xs) = {v | v =
        if (Set_mem x (listElts xs))
            then (Set_cup (Set_sng x) (dups xs))
            else (dups xs)}
@-}

Ух, крутяк, давайте теперь разбираться в этом. Первым делом мы определяем тип ListUnique, смысл его очевиден: уникальным является такой список, в котором нет повторяющихся элементов, то есть такой, для которого справедлив предикат NoDups. Он, в свою очередь, отражает такую ситуацию, в которой список повторяющихся элементов dups будет пустым. И вот тут начинается самое интересное.

Мы определяем measure (“измерение”) по имени dups. Воспринимайте measure как магическую функцию, ибо она выполняется не в процессе запуска программы, а в процессе статической верификации. А теперь взгляните на её реализацию. Видите функции с префиксом Set_? Это не просто функции, это тоже измерения, определённые в недрах пакета liquidhaskell. Но постойте, что-то в этих Set_ есть до боли знакомое… Так это же из Set взято! В самом деле Set_emp - это от предиката empty, а Set_mem - от предиката member. Так вот что мы сделали на самом деле! Мы определили рекурсивную функцию dups точно так же, как если бы мы просто писали обыкновенную живую проверку на уникальность. А магия liquid позволила нам определить соответствующие измерения и использовать их в момент верификации. Круто, правда?

И потому теперь мы можем написать так:

{-@ servicePorts :: ListUnique NotRootPort @-}
servicePorts :: [Port]
servicePorts =
  [3000, 3001, 3010, 3011, 3012, 3013
   3013, 3014, 3020, 3030, 3040, 3050]

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

Кроме того, обратите внимание на использование нашего старого знакомого NotRootPort. Liquid-типы можно комбинировать так же, как обычные Haskell-типы: мы определили уникальный список непривилигированных портов.

“Да, но ведь это всего лишь комментарии!”

Этот вопрос нельзя оставить без ответа. В самом деле, вся эта верификационная красота существует лишь в мире Haskell-комментариев. Значит, компилятор не воспрепятствует нам использовать ту же функцию okDiv для коварного деления на ноль!

Нет, не помешает. Но что помешает нам с вами прогонять команду liquid перед компиляцией? Мы смело можем делать это, ведь, как уже было сказано, внутри liquid используется ghc, а это значит, что помимо Liquid-типов проверяется и всё остальное. Это даёт нам важное преимущество: если команда liquid отработала успешно - значит и у компилятора претензий не будет. Так что открываем наш CI-конфиг (у нас ведь у всех есть такой, не правда ли?) и смело ставим шаг liquid-верификации перед шагом сборки. Если верификация не прошла - валим сборку как неудачную и идём в код разбираться, что к чему.

Ссылки

Дабы избавить вас от лишнего гугления, вот вам полезные ссылки.

Официальный сайт. Как обычно: ссылки на материалы по теме, а также интересные блогозаписи от авторов пакета.
GitHub-репозиторий. Кстати, на issue авторы отвечают весьма оперативно.
Онлайн-демонстрация. Да-да, всю эту красоту можно попробовать в браузере.
Презентация на LambdaConf 2015. Довольно длинная, но разжёвано хорошо.

И на десерт - поддержка LiquidHaskell для редакторов:

Признаться, я не пробовал эти расширения, так что пишите в комментариях, как они.

Продолжение следует…

Да, друзья, как бы ни хотелось мне продолжить, но шибко большие публикации воспринимаются тяжело. Так что ждите следующих заметок: поверьте, я рассказал про liquidhaskell не всё.