?

Log in

No account? Create an account

Previous Entry | Next Entry

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

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

Выглядит это так. Допустим, мы в отдельно компилируемом модуле описываем такую функцию:
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, который из типа простейшую реализацию изобретает, тут действительно переданная функция материализуется.

Как это работает и что должно быть там вместо троеточия?
Мы будем строить AST (абстрактное синтаксическое дерево бодхи) и потом из него получать строку. Для описания AST все настоящие йоги не используют алгебраические типы, т.к. есть более гибкий и расширяемый подход: typed tagless + HOAS, на тайпклассах. Стоит о нем рассказать подробнее. В базовом лямбда исчислении у нас есть всего три вещи: абстракция (создание безымянной функции), применение (вызов функции) и переменные (они возникают при описании функции - ее аргументы - и могут использоваться в выражениях). Первый приходящий на ум способ закодировать выражение - сделать алгебраический тип из трех вариантов, и переменные обозначать строками. Он очень неудобен тем, что придется много возиться с именами, реализовывать альфа-конверсию (переименовывание), чтобы обеспечить уникальность всех имен и отсутствие путаницы, когда одни выражения подставляются в другие, где есть переменные с такими же именами. Это лечат заменой имен переменных индексами de Bruijn'a, когда вместо упоминания переменной по имени используют натуральное число, означающее количество лямбда-абстракций на пути в дереве терма между определением нужной переменной и местом ее упоминания. Так, \x -> x превращается в Lam (Var 0), a \x -> \y -> x в Lam (Lam (Var 1)). При использовании HOAS (Higher-order abstract syntax) мы вообще не кодируем переменные термами объектного языка, а используем переменные и функции языка-хоста, на котором пишем. Тогда бестиповая лямбда кодируется алгебраическим типом из всего двух вариантов:
data Exp = App Exp Exp | Lam (Exp -> Exp)
Функция \x -> x кодируется как Lam (\x -> x), а \x -> \y -> x как Lam(\x -> Lam(\y -> x)).
Так у нас опять есть именованные переменные, но заботу об их именах и областях видимости теперь берет на себя компилятор хост-языка, в данном случае хаскеля. Чтобы из бестиповой лямбды сделать типизированную, добавим тип-параметр и запишем тип в виде GADT:
data Exp a where
  App :: Exp (a->b) -> Exp a -> Exp b
  Lam :: (Exp a -> Exp b) -> Exp (a->b)

Этот подход все еще недостаточно хорош: чтобы добавить в язык новые конструкции, например туплы, придется править этот тип. Добавлять дополнительную информацию к термам тоже неудобно. Expression problem в чистом виде. Решение же очень простое и сводится к паре переименований с заменой data на class:
class Lam repr where
  app :: repr (a -> b) -> repr a -> repr b
  lam :: (repr a -> repr b) -> repr (a -> b)

Опытный глаз сразу заметит в app знакомый метод <*> аппликативного функтора. А вот функция с обратным типом - lam - гораздо менее знаменита.
Выражения теперь строятся и выглядят в точности как раньше, только с маленькой буквы: lam (\x -> lam(\y -> x)). Но тип имеют не один фиксированный Exp something, а сразу много (полиморфный):
Lam repr => repr something
Реализуешь класс одним образом - получишь интерпретатор, другим - сериализатор, третьим - оптимизатор. Давайте сразу сделаем сериализацию в строку:
newtype StrRepr a = Str { unS :: Int -> String }

pns :: String -> String
pns s = "(" ++ s ++ ")"

instance Lam StrRepr where
  app f x = Str $ \n -> pns $ unS f n ++ " " ++ unS x n 
  lam f   = Str $ \n -> let x = "x" ++ show n in                    
                        pns $ "\\" ++ x ++ " -> " ++ (unS . f . Str $ const x) (n+1)

view :: StrRepr a -> String
view e = unS e 1

Теперь view $ lam (\x -> lam(\y -> x)) вернет нам "(\x1 -> (\x2 -> x1))". Идея в том, что когда мы строим термы, они еще не связаны ни с какой конкретной реализацией класса Lam, и мы можем один и тот же терм передавать в трактующие его по-разному функции. Например, view полученный терм трактует как StrRepr, и терм внезапно превращается в функцию из номера переменной в строку.

Самое хорошее, что теперь можно добавлять другие конструкции, и не придется менять исходный тип. Мы просто добавляем новые тайпклассы, и выражения строим с использованием функций из нескольких классов. Добавим туплы:
class Prod repr where
  pair :: (repr a, repr b) -> repr (a,b)
  pi1  :: repr (a,b) -> repr a
  pi2  :: repr (a,b) -> repr b

instance Prod StrRepr where
  pair (x, y) = Str $ \n -> pns $ unS x n ++ ", " ++ unS y n 
  pi1 p       = Str $ \n -> pns $ "fst " ++ unS p n 
  pi2 p       = Str $ \n -> pns $ "snd " ++ unS p n 

Теперь функцию, например, swap (a,b) = (b,a) мы можем представить таким термом:
swap :: (Lam repr, Prod repr) => repr ((a,b) -> (b,a))
swap = lam(\p -> pair (pi2 p, pi1 p))

и view swap вернет нам
"(\x1 -> ((snd x1), (fst x1)))"

Этот подход работает в хаскеле, окамле (там вместо тайпклассов модули) и в любом другом нормальном языке, кроме Идриса, где тайпклассы есть, но тайпчекер их простоват и на таких штуках не осиливает нужные типы сопоставить.

Итак, AST мы описали (типизированно и бестэгово: любая интерпретация происходит без матчинга по вариантам, терм представляет собой функцию, и она просто вызывается). Теперь обещанный фокус с материализацией. Мы хотим превратить функцию некоторого типа Т в терм типа repr T, который потом сможем вывести в строку. Нам пригодится конвертер - пара функций reify/reflect, переводящих из типов метаязыка (хоста) в термы-репрезентации и обратно.
data RR repr meta a = RR {reify   :: meta -> repr a,
                          reflect :: repr a -> meta} 

"repr a" равен сам себе, конверсия из него в него - просто id.
_t :: RR repr (repr a) a
_t = RR {reify = id, reflect = id}


Теперь рассмотрим простейшую функцию - тот же id = \x -> x. Она имеет тип a -> a, где вместо а можно поставить что угодно, в том числе repr a, т.е. мы ее можем использовать там, где нужно repr a -> repr a. Передав ее в lam, мы получим значение типа repr (a->a), т.е. получим ее представление в виде терма:
tid :: Lam repr => repr (a->a)
tid = lam id

Для более сложных функций, где слева и справа от стрелки разные типы (которые мы уже умеем конвертировать), конверсия чуть сложнее, но тоже сводится к применению lam. Если у нас есть функция из а в b, то, имея конвертеры между a и repr a, а также b и repr b, получить repr (a->b) мы можем, передав в lam функцию типа repr a -> repr b, получить которую из исходной мы можем, сконвертировав repr a в a, а результат b в repr b. Аналогично обратно:
infixr 8 -->			
(-->) :: Lam repr => RR repr m1 o1 -> RR repr m2 o2 -> RR repr (m1 -> m2) (o1 -> o2)
r1 --> r2 = RR {reify   = \m -> lam (reify r2 . m . reflect r1),
                reflect = \o -> reflect r2 . app o . reify r1 }

Еще нам нужен конвертер для туплов. Превратить пару значений в терм-пару термов, имея конвертеры для тех значений, не составляет труда:
_pair :: Prod repr => RR repr ta a -> RR repr tb b -> RR repr (ta,tb) (a,b)
_pair rx ry  = RR {reify   = \(x,y) -> pair (reify rx x, reify ry y),
                   reflect = \p -> (reflect rx $ pi1 p, reflect ry $ pi2 p) }


Вот и все. Из этих _t, --> и _pair мы можем построить конвертер для любой функции из заявленного подмножества языка, надо лишь взять ее тип и заменить полиморфные типы на _t, стрелки на -->, а туплы на _pair. Несколько примеров:
myfun :: (a -> b) -> (b -> a) -> a -> b
myfun f g x = f (g (f x))

term2 :: Lam repr => repr ((a -> b) -> (b -> a) -> a -> b)
term2 = reify ((_t --> _t) --> (_t --> _t) --> _t -->_t) myfun

fun3 :: (a, b) -> a
fun3 p = fst p

term3 :: (Lam repr, Prod repr) => repr ((a,b) -> a)
term3 = reify (_pair _t _t --> _t) fun3

term :: (Lam repr, Prod repr) => repr ((a, (b, c)) -> (b -> b) -> (b -> a) -> ((b, a), c))
term = reify (_pair _t (_pair _t _t) --> (_t --> _t) --> (_t --> _t) --> 
              _pair (_pair _t _t) _t) some_fun

*Main> view term2
"(\x1 -> (\x2 -> (\x3 -> (x1 (x2 (x1 x3))))))"
*Main> view term3
"(\x1 -> (fst x1))"
*Main> view term
"(\x1 -> (\x2 -> (\x3 -> (((x2 (x2 (fst (snd x1)))), (x3 (x2 (fst (snd x1))))), (snd (snd x1))))))"


Так-то. А теперь домашнее задание: добавить сюда sum type (Either). У меня там получилось сделать reify, но не получилось сделать reflect, потому конвертер не написался.

Tags:

Comments

( 32 comments — Leave a comment )
xeno_by
Jul. 23rd, 2013 03:00 pm (UTC)
К вопросу, где это может быть применимо: http://scala-lms.github.io/. (Наверняка, уважаемый автор про сабж знает, поэтому я, в основном, для читателей).
xeno_by
Jul. 23rd, 2013 03:03 pm (UTC)
Ага, тут не совсем то! Сигнатура оригинальной функции не меняется и все равно ее получается реифицировать!
(no subject) - xeno_by - Jul. 23rd, 2013 03:25 pm (UTC) - Expand
ex_juan_gan
Jul. 23rd, 2013 03:08 pm (UTC)
О блин. Запрограммировали всё, что можно запрограммировать.
xeno_by
Jul. 23rd, 2013 03:10 pm (UTC)
Кстати, а как настоящие йоги представляют сниппеты кодяры, которые сами по себе не тайпчекаются?

1) Полезно иметь возможность наколбасить в разных местах кусочки кода, которые потом объединяются в единое целое. Зачастую выходит так, что эти кусочки имеют смысл только в контексте других (например, используют переменные, объявленные где-то еще), поэтому выразить их в виде HOAS не получится. Что делать?

2) Также полезно в научных целях разбирать сниппеты на запчасти. Как это записать в HOAS? Как таким запчастям назначить типы?
thedeemon
Jul. 23rd, 2013 03:43 pm (UTC)
Хороший вопрос. Полагаю, настоящие йоги не допускают даже мыслей о нетайпчекающихся сниппетах. Оперируй замкнутыми термами, так познаешь Брахмана!
xeno_by
Jul. 23rd, 2013 03:24 pm (UTC)
Получается, что для реализации своего трюка ты: 1) собираешь реифицированную сигнатуру руками, 2) выщемливаешь из нее аргументы, которые не стыдно передать в функцию, 3) вызываешь функцию, по сути, выполняя symbolic execution, 4) выщемливаешь из сигнатуры возвращаемый тип и на основе него обрабатываешь результат вызова функции. Правильно?

А теперь вопрос. Можно ли сделать такой реифай, чтобы можно было написать просто "reify myfun", без всяких многоточий? Можно ли реифицированную сигнатуру генерировать каким-нибудь хитрым тайпклассом, например?

Ну и плюс. Как это обобщить для конкретных типов, например, если myfun принимает Int и возвращает Int?

Edited at 2013-07-23 07:34 pm (UTC)
thedeemon
Jul. 23rd, 2013 03:49 pm (UTC)
Вроде того.

Просто "reify myfun" было бы здорово, но как этого добиться я пока не знаю.

С конкретными типами эта магия не работает, ибо все строится на том, что передаваемая функция всеядна и переварит волшебную пилюлю. Так что практического применения тут немного, только в цирке выступать.
(Deleted comment)
xeno_by
Jul. 23rd, 2013 03:43 pm (UTC)
>>Опытный глаз сразу заметит в app знакомый метод <*> аппликативного функтора. А вот функция с обратным типом - lam - гораздо менее знаменита.

Можешь вот это пояснить? Получается, есть какая-то алгебраическая структура, соответствующая метапрограммированию (т.е. манипуляциям над Code[T])? Какие у нее есть интересные законы?
thedeemon
Jul. 23rd, 2013 03:52 pm (UTC)
Речь об этом:
http://www.haskell.org/ghc/docs/latest/html/libraries/base/Control-Applicative.html

Об аппликативных функторах (коими в ЯП все монады являются, в частности) и их чудодейственных свойствах написаны тома.
maxim
Jul. 23rd, 2013 03:45 pm (UTC)
Слава, О, Великий, Лямбдагарбха!
diam_2003
Jul. 23rd, 2013 03:55 pm (UTC)
От, цэ кошерно.
nivanych
Jul. 23rd, 2013 11:17 pm (UTC)
> кроме Идриса, где тайпклассы есть

Получается, что и кроме CoQ.
Ну и, в известном смысле, кроме агдочки.
thedeemon
Jul. 24th, 2013 02:03 am (UTC)
А окамло-смле-подобных модулей в коке нет?
(no subject) - nivanych - Jul. 24th, 2013 02:08 am (UTC) - Expand
(no subject) - Алексей Егоров - Jul. 25th, 2013 12:12 am (UTC) - Expand
dima_starosud
Jul. 24th, 2013 02:15 am (UTC)
HOAS - крутая штука, надо будет попробовать (а то писал похожую вещь но с переменными, переименовыванием, и застопорившись, закинул).

И вопрос. Вы добавляете разные штуки (кортеж, сумма). Можно ли обойтись без этого? Я имею ввиду писать не так:
_pair _t _t --> _t
а так:
x --> (x --> t) --> (x --> t) --> t
(x - это кортеж, а (x --> t) функция для работы с ним, возвращающая его первый (и второй, так как типы их одинаковы в данном примере) элемент)
То есть передавать весь существующий контекст, как аргументы.
thedeemon
Jul. 24th, 2013 03:25 am (UTC)
Форма конвертера соответствует типу передаваемой функции. Скажем, swap принимает один аргумент - кортеж, и если использовать, как предлагаете, Church encoding, то конвертер будет ожидать функцию с большим числом аргументов. Типы не сойдутся.
helvegr
Jul. 24th, 2013 02:36 am (UTC)
Клёво.
theiced
Jul. 24th, 2013 03:00 am (UTC)
а зачем весь этот ад? :)
thedeemon
Jul. 24th, 2013 03:19 am (UTC)
20 пфеннингов за билет!
(no subject) - sassa_nf - Jul. 24th, 2013 06:31 am (UTC) - Expand
(no subject) - xeno_by - Jul. 24th, 2013 06:34 am (UTC) - Expand
beroal
Sep. 27th, 2013 07:32 am (UTC)
Вы ищете доказательство в пропозициональной интуиционистской логике? Используете её разрешимость?

Edited at 2013-09-27 11:34 am (UTC)
thedeemon
Sep. 27th, 2013 08:07 am (UTC)
Нет, не ищу, я его беру на вход и превращаю в строку.
sassa_nf
Jul. 7th, 2015 09:53 am (UTC)
а можно передать вопрос Лямбдагарбхе?

а ну-ка, как там обстоят дела с реификацией Either? (даже не с рефлектом)
thedeemon
Jul. 7th, 2015 09:55 am (UTC)
См. последний абзац поста.
А, если нужен код, то это мне надо поискать в бэкапах, он на старом ноуте был.

Edited at 2015-07-07 12:59 pm (UTC)
(no subject) - sassa_nf - Jul. 7th, 2015 10:22 am (UTC) - Expand
(no subject) - sassa_nf - Jul. 7th, 2015 11:54 am (UTC) - Expand
(no subject) - thedeemon - Jul. 8th, 2015 07:57 am (UTC) - Expand
(no subject) - sassa_nf - Jul. 8th, 2015 08:13 am (UTC) - Expand
( 32 comments — Leave a comment )