Идея заключается в том, чтобы усилить identity type так, чтобы больше вещей можно было доказать "в одно действие" через аналог идрисовского replace (названный в лекциях subst):
replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
Для этого из
- "рефлом", т.е. definitionally equal terms
refl (A : U) (a : A) : Path A a a
- экстенсионально равными функциями (версия для dependent product тоже есть)
funExtNonDep (A B: U) (f g : A -> B) (p : (x : A) -> Path B (f x) (g x)) : Path (A -> B) f g
- изоморфными типами (т.е. если у нас есть функция между значениями типов A и B с левой и правой обратной - то типы "равны"):
isoPath (A B : U) (f : A -> B) (g : B -> A)
(s : (y : B) -> Path B (f (g y)) y)
(t : (x : A) -> Path A (g (f x)) x) : Path U A BИнтересно, что всё это работает и с функциями уровня типов.В результате можно написать такую функцию:
functor_transport (F G: U -> U) (p: Path (U -> U) F G) (f: functor F): functor G = subst (U -> U) functor F G p fТо есть, для изоморфных типов F и G (с кайндами * -> * в терминах х-я) по инстансу функтора для F можно родить инстанс для G, при этом тело и сигнатуры fmap и теоремы о соблюдении законов функтора переписываются "автомагически".
Ну а дальше оказывается, что изоморфизмы у нас повсеместно. Скажем, таплы у самоизоморфны - т.е. есть Path U (A, B) (B, A), ну и из (first, fst, functorForA) "в одно действие" получаются (second, snd, functorForB). А дальше из (first, fst, functorForA, second, snd, functorForB) "в одно действие" получается реализация 6 функций и док-во 4 теорем (1 ф-ция и 2 теоремы внутри functorA/B сидят) для пар в кодировках чёрча и остальных over 9000 возможных представлений пар.
Ну, на самом деле требуется доказать в каждом случае соответствующий Path, но это проще чем передоказывать теоремы.
Кроме того, есть техника метапрограммирования: есть изоморфизм bool самого с собой (через not). И мы можем написать функцию, автомагически заменяющую все булы в любом терме вида F bool на их отрицания (и функции что самое смешное тоже переписываются). Типа
data food = cheese | beef | chicken
-- Predicate encoding which food someone eats
eats (X : U) : U = list (and food X)
anders : eats bool = cons (cheese,true)
(cons (beef,false)
(cons (chicken,false) nil))
-- Cyril eats the complement of Anders
cyril : eats bool = substEquiv eats bool bool notEquiv andersnotEquiv тут как раз доказательство изоморфизма. Ну и понятно что заменяются не все вхождения Bool, а "все вхождения в позициях, отмеченных Х". Любопытно, что код ничего не знает о том как обходить списки - у нас нету fmap для eats :)Дебильные комментарии, комментарии "практиков" и школьников - как обычно, скринятся. RTFM, do you homework, пиши развёрнуто и конструктивно! https://t.me/groupoid (но там банхаммер, так что лучше сюда)
