колдунство реификации
Jul. 23rd, 2013 10:53 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
thedeemonДамы и господа! Не проходите мимо! Только сегодня в нашем бродячем цирке великий йог и аскет Лямбдагарбха продемонстрирует уникальный фокус материализации! Имея полиморфную функцию, оперирующую произвольными типами (полифорфными, не конкретными), функциями из них и туплами, только зная ее тип и умея ее вызывать, он материализует ее исходник, даже если она скомпилирована в другом городе, и никакое ее оригинальное представление уже не доступно.
Выглядит это так. Допустим, мы в отдельно компилируемом модуле описываем такую функцию:
В ней не упоминаются числа, строки и другие конкретные типы, но есть пары и функции. Теперь мы в другом модуле пишем
И получаем в 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:
Этот подход все еще недостаточно хорош: чтобы добавить в язык новые конструкции, например туплы, придется править этот тип. Добавлять дополнительную информацию к термам тоже неудобно. Expression problem в чистом виде. Решение же очень простое и сводится к паре переименований с заменой data на class:
Опытный глаз сразу заметит в app знакомый метод <*> аппликативного функтора. А вот функция с обратным типом - lam - гораздо менее знаменита.
Выражения теперь строятся и выглядят в точности как раньше, только с маленькой буквы: lam (\x -> lam(\y -> x)). Но тип имеют не один фиксированный Exp something, а сразу много (полиморфный):
Lam repr => repr something
Реализуешь класс одним образом - получишь интерпретатор, другим - сериализатор, третьим - оптимизатор. Давайте сразу сделаем сериализацию в строку:
Теперь view $ lam (\x -> lam(\y -> x)) вернет нам "(\x1 -> (\x2 -> x1))". Идея в том, что когда мы строим термы, они еще не связаны ни с какой конкретной реализацией класса Lam, и мы можем один и тот же терм передавать в трактующие его по-разному функции. Например, view полученный терм трактует как StrRepr, и терм внезапно превращается в функцию из номера переменной в строку.
Самое хорошее, что теперь можно добавлять другие конструкции, и не придется менять исходный тип. Мы просто добавляем новые тайпклассы, и выражения строим с использованием функций из нескольких классов. Добавим туплы:
Теперь функцию, например, swap (a,b) = (b,a) мы можем представить таким термом:
и view swap вернет нам
"(\x1 -> ((snd x1), (fst x1)))"
Этот подход работает в хаскеле, окамле (там вместо тайпклассов модули) и в любом другом нормальном языке, кроме Идриса, где тайпклассы есть, но тайпчекер их простоват и на таких штуках не осиливает нужные типы сопоставить.
Итак, AST мы описали (типизированно и бестэгово: любая интерпретация происходит без матчинга по вариантам, терм представляет собой функцию, и она просто вызывается). Теперь обещанный фокус с материализацией. Мы хотим превратить функцию некоторого типа Т в терм типа repr T, который потом сможем вывести в строку. Нам пригодится конвертер - пара функций reify/reflect, переводящих из типов метаязыка (хоста) в термы-репрезентации и обратно.
"repr a" равен сам себе, конверсия из него в него - просто id.
Теперь рассмотрим простейшую функцию - тот же id = \x -> x. Она имеет тип a -> a, где вместо а можно поставить что угодно, в том числе repr a, т.е. мы ее можем использовать там, где нужно repr a -> repr a. Передав ее в lam, мы получим значение типа repr (a->a), т.е. получим ее представление в виде терма:
Для более сложных функций, где слева и справа от стрелки разные типы (которые мы уже умеем конвертировать), конверсия чуть сложнее, но тоже сводится к применению lam. Если у нас есть функция из а в b, то, имея конвертеры между a и repr a, а также b и repr b, получить repr (a->b) мы можем, передав в lam функцию типа repr a -> repr b, получить которую из исходной мы можем, сконвертировав repr a в a, а результат b в repr b. Аналогично обратно:
Еще нам нужен конвертер для туплов. Превратить пару значений в терм-пару термов, имея конвертеры для тех значений, не составляет труда:
Вот и все. Из этих _t, --> и _pair мы можем построить конвертер для любой функции из заявленного подмножества языка, надо лишь взять ее тип и заменить полиморфные типы на _t, стрелки на -->, а туплы на _pair. Несколько примеров:
Так-то. А теперь домашнее задание: добавить сюда sum type (Either). У меня там получилось сделать reify, но не получилось сделать reflect, потому конвертер не написался.
Выглядит это так. Допустим, мы в отдельно компилируемом модуле описываем такую функцию:
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, потому конвертер не написался.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2013-07-23 07:00 pm (UTC)no subject
Date: 2013-07-23 07:03 pm (UTC)no subject
Date: 2013-07-23 07:25 pm (UTC)no subject
Date: 2013-07-23 07:08 pm (UTC)no subject
Date: 2013-07-23 07:10 pm (UTC)1) Полезно иметь возможность наколбасить в разных местах кусочки кода, которые потом объединяются в единое целое. Зачастую выходит так, что эти кусочки имеют смысл только в контексте других (например, используют переменные, объявленные где-то еще), поэтому выразить их в виде HOAS не получится. Что делать?
2) Также полезно в научных целях разбирать сниппеты на запчасти. Как это записать в HOAS? Как таким запчастям назначить типы?
no subject
Date: 2013-07-23 07:43 pm (UTC)no subject
Date: 2013-07-23 07:24 pm (UTC)А теперь вопрос. Можно ли сделать такой реифай, чтобы можно было написать просто "reify myfun", без всяких многоточий? Можно ли реифицированную сигнатуру генерировать каким-нибудь хитрым тайпклассом, например?
Ну и плюс. Как это обобщить для конкретных типов, например, если myfun принимает Int и возвращает Int?
no subject
Date: 2013-07-23 07:49 pm (UTC)Просто "reify myfun" было бы здорово, но как этого добиться я пока не знаю.
С конкретными типами эта магия не работает, ибо все строится на том, что передаваемая функция всеядна и переварит волшебную пилюлю. Так что практического применения тут немного, только в цирке выступать.
no subject
Date: 2013-07-23 07:37 pm (UTC)no subject
Date: 2013-07-23 07:43 pm (UTC)Можешь вот это пояснить? Получается, есть какая-то алгебраическая структура, соответствующая метапрограммированию (т.е. манипуляциям над Code[T])? Какие у нее есть интересные законы?
no subject
Date: 2013-07-23 07:52 pm (UTC)http://www.haskell.org/ghc/docs/latest/html/libraries/base/Control-Applicative.html
Об аппликативных функторах (коими в ЯП все монады являются, в частности) и их чудодейственных свойствах написаны тома.
no subject
Date: 2013-07-23 07:45 pm (UTC)no subject
Date: 2013-07-23 07:55 pm (UTC)no subject
Date: 2013-07-24 03:17 am (UTC)Получается, что и кроме CoQ.
Ну и, в известном смысле, кроме агдочки.
no subject
Date: 2013-07-24 06:03 am (UTC)no subject
Date: 2013-07-24 06:08 am (UTC)Но я просто попытался про его классотипы вспомнить.
Ну и давно уже с CoQ возился, могу что-то забыть и перепутать.
no subject
Date: 2013-07-25 04:12 am (UTC)type App r a b = r (a -> b) -> r a -> r b
type Abs r a b = (r a -> r b) -> r (a -> b)
type Lam r a b t = (App r a b, (Abs r a b, t))
app :: Lam r a b t -> App r a b
app (a, _) = a
abs :: Lam r a b t -> Abs r a b
abs (_, (a,_)) = a
Тип словаря при этом остается расширяемым за счет параметра t.
no subject
Date: 2013-07-24 06:15 am (UTC)И вопрос. Вы добавляете разные штуки (кортеж, сумма). Можно ли обойтись без этого? Я имею ввиду писать не так:
_pair _t _t --> _t
а так:
x --> (x --> t) --> (x --> t) --> t
(x - это кортеж, а (x --> t) функция для работы с ним, возвращающая его первый (и второй, так как типы их одинаковы в данном примере) элемент)
То есть передавать весь существующий контекст, как аргументы.
no subject
Date: 2013-07-24 07:25 am (UTC)no subject
Date: 2013-07-24 06:36 am (UTC)no subject
Date: 2013-07-24 07:00 am (UTC)no subject
Date: 2013-07-24 07:19 am (UTC)no subject
Date: 2013-07-24 10:31 am (UTC)no subject
Date: 2013-07-24 10:34 am (UTC)no subject
Date: 2013-09-27 11:32 am (UTC)no subject
Date: 2013-09-27 12:07 pm (UTC)no subject
Date: 2015-07-07 12:53 pm (UTC)а ну-ка, как там обстоят дела с реификацией Either? (даже не с рефлектом)
no subject
Date: 2015-07-07 12:55 pm (UTC)А, если нужен код, то это мне надо поискать в бэкапах, он на старом ноуте был.
no subject
Date: 2015-07-07 01:22 pm (UTC)а то у меня выходит, что нужно различать ко- и контра-вариантные употребления Either. Ломаю голову, почему с туплями такого нет.
no subject
Date: 2015-07-07 02:54 pm (UTC)а именно. Для reify нам нужен способ repr (a,b)->(repr a, repr b). Для туплей это возможно получить, применяя fst и snd. То есть, получаем \x -> (fst x, fst y) там, где можно было бы \(x,y) -> (x,y). Но reify . reflect отнюдь не id, поэтому получаем:
print $ view $ reify (_t --> (_pair _t _t)) $ reflect (_t --> (_pair _t _t)) $ reify (_t --> (_pair _t _t)) $ reflect (_t --> (_pair _t _t)) $ reify (_t --> (_pair _t _t)) (\x -> (x,x))(\\x1 -> ((fst ((\\x2 -> ((fst ((\\x3 -> (x3, x3)) x2)), (snd ((\\x3 -> (x3, x3)) x2)))) x1)), (snd ((\\x2 -> ((fst ((\\x3 -> (x3, x3)) x2)), (snd ((\\x3 -> (x3, x3)) x2)))) x1))))
По-хорошему нужно было бы парсить строку, чтобы из repr (a,b) получить repr a и repr b.
no subject
Date: 2015-07-08 10:57 am (UTC)class Sum repr where left :: repr a -> repr (Either a b) right :: repr b -> repr (Either a b) match :: repr (Either a b) -> repr (a -> c) -> repr (b -> c) -> repr c instance Sum StrRepr where left x = Str $ \n -> "Left " ++ unS x n right x = Str $ \n -> "Right " ++ unS x n match e fa fb = Str $ \n -> "case " ++ unS e n ++ " of Left " ++ unS fa n ++ "| Right" ++ unS fb n _either :: Sum repr => RR repr ta a -> RR repr tb b -> RR repr (Either ta tb) (Either a b) _either rx ry = RR {reify = \xy -> case xy of Left x -> left $ reify rx x Right y -> right $ reify ry y, reflect = undefined }no subject
Date: 2015-07-08 11:13 am (UTC)У меня наподобие. Маленькая проблемка: кто-то где-то должен вбросить все возможные варианты аргументов в функцию от Either - чтобы отобразить все ветки кейса.
Например: f :: Either (Either a b) c -> Either a (Either b c) - нужно уметь вбросить три варианта на вход, или писать f другим способом, через either, который сейчас подаётся из Prelude, а должно из тайп-класса контекста.
Вот в этом месте и появляется необходимость отличать ковариантное использование Either (получаем _either как у Лямбдагарбхи), и контравариантное использование Either (должны получить что-то, что перебирает все варианты заворачивания значения аргумента для функции, и по нему строит функцию с кейс-матчем)