Неизвестная Миру Лямбда Кодировка с CPS Континуатором
НАМО ЛЯМБДАГАРБХА
Итак, как вы все знаете, в PTS системах для кодирования индуктивных типов данных принято использовать лямбда исчисление. Все вы знаете про Church, Parigot, Scott кодировки. Если кто забыл, я быстро напомню! Но есть одна особая кодировка, которая круче чем все эти кодировки, но которая почему-то совершенно не описана в литературе, но описана была MaiaVictor. Его же синтаксис Caramel использовался для демонстрации всех кодировок в нетипизированном лямбда исчислении.
Будем использовать инфиксную скобочную форму записи лямбды: "(a b -> c)" означает "λ a b . c", чтобы λ не мусолила глаза и легче было распознавать узор последовательности.
Church кодировка
Самая простая. Она представляет структуры в виде своих правых фолдов. Будем рассматривать простейшие структуры данных натуральные числа. Они же используются дя чистого моделирования вселенных.
0 = (f x -> x)
1 = (f x -> (f x))
2 = (f x -> (f (f x)))
3 = (f x -> (f (f (f x))))
pred = (n (g h -> (h (g succ))) (const zero) id) — O(n), плохо.
foldNat = (s z nat -> (nat s z)) — Нерекурсивный, хорошо.
С ней есть "маленькая" проблемка: pred такого числа или tail списка занимает O(n).
Scott кодировка
Дана Скотт предложил кодирвать структуры не в виде их фолдов а в виде их паттерн мачинг элиминаторов.
0 = (f x -> x)
1 = (f x -> (f (f x -> x)))
2 = (f x -> (f (f x -> (f (f x -> x)))))
3 = (f x -> (f (f x -> (f (f x -> (f (f x -> x)))))))
pred = (nat -> (nat (pred -> pred) _)) — O(1), хорошо.
foldNat = (s z nat -> (nat (pred -> (s (foldNat s z pred))) z)) — Рекурсия, плохо.
Для такой кодировки у нас pred натурального числа занимает константу, но для выражения нужна рекурсия. А мы на это в Групоид Инфинити никак не можем пойти.
Кодировка Parigot
Является смесью Скотт и Черч кодировок. Паригот убирает рекурсию из фолдов.
0 = (f x -> x)
1 = (f x -> (f (f x -> (f x)) (f x -> x)))
2 = (f x -> (f (f x -> (f (f x))) (f x -> (f (f x -> (f x)) (f x -> x)))))
3 = (f x -> (f (f x -> (f (f (f x)))) (f x -> (f (f x -> (f (f x))) (f x -> (f (f x -> (f x)) (f x -> x)))))))
pred = (nat -> (nat (_ pred -> pred) _)) -- O(1), хорошо.
foldNat = (nat -> (nat (fold _ -> fold) _)) -- нерекурсивный, хорошо.
Как вы видите Паригот вроде как заебись, но термы ростут как на дрожжах. Т.е. экспоненциально. Но мы можем избавиться от этого!
Кодировка CPS
Вместо нумералов черча мы храним континуаторы (c -> (c f x)). Описание этой кодировки вы не найдете в интернете ни в одном пейпере.
0 = (f x -> x)
1 = (f x -> (f (c -> (c f x)) (f x -> x)))
2 = (f x -> (f (c -> (c f x)) (f x -> (f (c -> (c f x)) (f x -> x)))))
3 = (f x -> (f (c -> (c f x)) (f x -> (f (c -> (c f x)) (f x -> (f (c -> (c f x)) (f x -> x)))))))
pred = (nat -> (nat (_ pred -> pred) _)) — O(1), хорошо!
foldNat = (s z nat -> (nat (cont pred -> (s (cont pred))) z)) — нерекурсивная, хорошо!
И термы все растут так как при черче просто умножаются на константу -- размер континуатора. Одна хуйня что для этой кодировки нужны Self-типы Пенг-Фу и Ко, слабая форма рекурсивных типов. Но зато индукция и все остальное получается бесплатно для этой кодировки.
Бенчмарк CPS кодирвки против Church кодировки:
Pack/Unpack 1 000 000 Inductive Nat Church: {410682,#Fun}
Pack/Unpack 1 000 000 Inductive Nat CPS: {712684,1000000}
Pack/Unpack 1 000 000 Inductive Church List: {717695,'_'}
Типа в два раз медленнее.
data nat : * | (zero: () → nat)
| (succ: nat → nat)
Church
nat () -> [fun (S) -> 1 + S end, 0 ].
zero () -> fun (S) -> fun (Z) -> Z end end.
succ () -> fun (N) -> fun (S)
-> fun (Z) -> S((N(S))(Z)) end end end.
CPS
nat1() -> [fun (F) -> fun (X) -> F(X) + 1 end end, 0 ].
zero1() -> fun (F) -> fun (X) -> X end end.
succ1() -> fun (Z) -> fun (F) -> fun (X)
-> (F(fun(C) -> (C(F))(X) end))(Z) end end end.
ОМ ЛЯМБДА ГАРБХА ХУМ