колдунство реификации
Дамы и господа! Не проходите мимо! Только сегодня в нашем бродячем цирке великий йог и аскет Лямбдагарбха продемонстрирует уникальный фокус материализации! Имея полиморфную функцию, оперирующую произвольными типами (полифорфными, не конкретными), функциями из них и туплами, только зная ее тип и умея ее вызывать, он материализует ее исходник, даже если она скомпилирована в другом городе, и никакое ее оригинальное представление уже не доступно.
Выглядит это так. Допустим, мы в отдельно компилируемом модуле описываем такую функцию:
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, потому конвертер не написался.
Выглядит это так. Допустим, мы в отдельно компилируемом модуле описываем такую функцию:
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, потому конвертер не написался.