колдунство реификации

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

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

some_fun :: (a, (b, c)) -> (b -> b) -> (b -> a) -> ((b, a), c)
some_fun (a,(b,c)) f g = ((f . f $ b, g . f $ b), c)

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

term = reify ... some_fun
result :: String
result = view term

И получаем в result строку
"(\x1 -> (\x2 -> (\x3 -> (((x2 (x2 (fst (snd x1)))), (x3 (x2 (fst (snd x1))))), (snd (snd x1))))))"
которая правдиво воспроизводит внутреннее устройство some_fun, только без имен переменных и синтаксического сахара. В частности, видно, что второй аргумент действительно применяется нужное число раз, из одного только типа это вывести невозможно, это не djinn, который из типа простейшую реализацию изобретает, тут действительно переданная функция материализуется.

Как это работает и что должно быть там вместо троеточия?( Read more... )