Магия Haskell - вызываем джина

Дата: November 30, 2014

Метки: haskell, djinn, windows

В мире Haskell есть много интересных пакетов, программ, которых не встретишь в мире ООП ввиду их функциональной направленности. Примером одной из таких программ является djinn, которую создал Lennart Augustsson (исходный код). То, что она делает, похоже на уличную магию и, видимо, производит наибольший вау-эффект на тех, кто недавно вошел в мир функционального программирования. Программа по заданному типу функции пытается сгенерировать код этой функции, если это вообще возможно. Лучше наверное сказать, что она, исходя из типов входных параметров, пытается найти такую трансформацию, которая бы в итоге возвращала значение нужного типа. Лучше всего это объяснить на примерах.

Как вызывать джина без лампы?

Для начала установим djinn. Актуальной версией на момент написания является 2014.9.7. Проблем с установкой под Windows быть не должно (обычно, если какая-либо программа на Haskell не собирается, то, как правило, не собирается именно под Windows, это если авторы использовали что-то из мира Linux, а именно в том мире в большинстве случаев обитают хаскеллисты).

Обновляем список пакетов и устанавливаем djinn:

> cabal update
> cabal install djinn

Все пакеты под Windows устанавливаются в %APPDATA%\cabal, устанавливаемые исполняемые файлы оказываются в каталоге %APPDATA%\cabal\bin, поэтому лучше всего добавить этот каталог в %PATH%, если этого еще не сделали. Все кто против системы или просто лентяи могут призвать джина путем запуска:

> %APPDATA%\cabal\bin\djinn.exe

Загадываем желания

Теперь, когда джин вызван, можно загадывать желания. Рассмотрим команды, которые он умеет выполнять.

Команда <sym> ? <type>

Эта команда используется чтобы сгенерировать функцию с именем <sym> по ее типу <type>. Djinn знает о типах функций, о кортежах, о Either, Maybe, (), можно также объявить и передать синонимы типов, тип данных. Вот список синонимов типов, типов данных и классов типов определенных в окружении djinn сразу после запуска (позже можно определить свои):

Djinn> :e
data () = ()
data Either a b = Left a | Right b
data Maybe a = Nothing | Just a
data Bool = False | True
data Void
type Not x = x -> Void
class Monad m where return :: a -> m a; (>>=) :: m a -> (a -> m b) -> m b
class Eq a where (==) :: a -> a -> Bool

Если функция может быть найдена, она будет выведена в виде кода на Haskell. Например, сгенерируем функцию, которая принимает параметр типа a и возвращает результат того же типа a:

Djinn> f ? a->a
f :: a -> a
f a = a

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

Djinn> sel ? ((a,b),(c,d)) -> (b,c)
sel :: ((a, b), (c, d)) -> (b, c)
sel ((_, a), (b, _)) = (a, b)

А слабо из типа a вывести тип b?

Djinn> convert ? a->b
-- convert cannot be realized.

“Ага-aa!!!” — укоризненно сказали суровые сибирские лесорубы.

Стоит также отметить, что если может быть несколько имплементаций, то будет выведена только одна из них. Например,

Djinn> f ? a->a->a
f :: a -> a -> a
f _ a = a

Однако, можно включить вывод нескольких решений командой:

Djinn> :s +multi

Тогда результат команды

Djinn> f ? a->a->a

будет таким

f :: a -> a -> a
f _ a = a
-- or
f a _ = a

Команда type <sym> <vars> = <type>

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

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

Djinn> type Id a = a->a
Djinn> f ? Id a
f :: Id a
f a = a

Пример посложнее. Попробуем найти реализацию функций return, bind и callCC для монады продолжения. Несколько описаний на английском этой монады есть в блоге Gabriel Gonzalez, Wikibooks, Stackoverflow FPComplete, на русском можно почитать на habrahabr, еще habrahabr, rsdn.

Djinn> type C r a = (a -> r) -> r
Djinn> returnC ? a -> C r a
returnC :: a -> C r a
returnC a b = b a
Djinn> bindC ? C r a -> (a -> C r b) -> C r b
bindC :: C r a -> (a -> C r b) -> C r b
bindC a b c = a (\ d -> b d c)
Djinn> callCC ? ((a -> C r b) -> C r a) -> C r a
callCC :: ((a -> C r b) -> C r a) -> C r a
callCC a b = a (\ c _ -> b c) b

Команда data <sym> <vars> = <type>

Эта команда добавляет в окружение новый тип данных.

Djinn> data Foo a = C a a a
Djinn> f ? a -> Foo a
f :: a -> Foo a
f a = C a a a

Стоит заметить, что djinn не позволяет определять рекурсивных типов. Т.е. если вы попытаетесь определить числа Пеано, djinn вас разочарует:

Djinn> data Peano = Zero | Succ Peano
Error: Recursive types are not allowed: Peano

Хотя djinn и позволяет определять пустые типы командой data <sym> <vars> (тип данных без конструкторов), но все они интерпретируются как одинаковые (из-за хака использованного при определении типов данных в djinn).

Можно теперь завернуть монаду продолжения в наш тип данных и посмотреть на результат генерации функций return, bind и callCC:

Djinn> data C r a = C ((a -> r) -> r)
Djinn> returnC ? a -> C r a
returnC :: a -> C r a
returnC a = C (\ b -> b a)
Djinn> bindC ? C r a -> (a -> C r b) -> C r b
bindC :: C r a -> (a -> C r b) -> C r b
bindC a b =
        case a of
        C c -> C (\ d ->
                  c (\ e ->
                     case b e of
                     C f -> f d))
Djinn> callCC ? ((a -> C r b) -> C r a) -> C r a
callCC :: ((a -> C r b) -> C r a) -> C r a
callCC a =
         C (\ b ->
            case a (\ c -> C (\ _ -> b c)) of
            C d -> d b)

Получилось не так красиво, как с синонимом типов, но дальше можно уже допилить напильником трансформируя case в патттерн матчинг на уровне параметров функции, например.

Команда ?instance <sym> <types>

Для того, чтобы не просить сгенерировать отдельно функции bind и return, можно попросить сразу сгенерировать инстанс класса типов Monad. Пример монады продолжения:

Djinn> data C r a = C ((a -> r) -> r)
Djinn> ?instance Monad (C r)
instance Monad (C r) where
   return a = C (\ b -> b a)
   (>>=) a b =
        case a of
        C c -> C (\ d ->
                  c (\ e ->
                     case b e of
                     C f -> f d))

Пример монады Maybe:

Djinn> ?instance Monad Maybe
instance Monad Maybe where
   return = Just
   (>>=) a b =
        case a of
        Nothing -> Nothing
        Just c -> b c

Команда class <sym> <vars> where <methods>

Никто не мешает определить свой класс типов и потом просить сгенерировать для этого класса типов реализацию.

Djinn> class Functor f where fmap :: (a -> b) -> f a -> f b; (<$) :: a -> f b -> f a
Djinn> ?instance Functor Maybe
instance Functor Maybe where
   fmap a b =
       case b of
       Nothing -> Nothing
       Just c -> Just (a c)
   (<$) a b =
       case b of
       Nothing -> Nothing
       Just _ -> Just a
Djinn> data C r a = C ((a -> r) -> r)
Djinn> ?instance Functor (C r)
instance Functor (C r) where
   fmap a b =
       case b of
       C c -> C (\ d -> c (\ e -> d (a e)))
   (<$) a b =
       case b of
       C c -> C (\ d -> c (\ _ -> d a))

Этих команд джину должно хватить, чтобы почувствовать себя магом в Haskell. Не упомянул я только команд

:clear                             Очистить окружение
:delete <sym>                      Удалить определенный символ из окружения
:help                              Вывести список команд
:load <file>                       Загрузить файл с командами
:quit                              Выйти из программы
:set <option>                      Установить опции джина

Можно использовать первые буквы команд. Опции по-умолчанию:

    -multi     Вывод нескольких решений
    +sorted    Сортировка решений
    -debug     Отладочный режим
    cutoff=200 Максимальное число генерируемых решений

Удачных заклинаний!

comments powered by Disqus