?

Log in

No account? Create an account
Унивалентность на кубических типах - Дважды мудак [entries|archive|friends|userinfo]
Декларативное рулит

Site Meter

[ website | Мой сайт ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Унивалентность на кубических типах [ноя. 7, 2017|16:37 pm]
Andy Melnikov
[Tags|, , ]

https://github.com/mortberg/cubicaltt/tree/master/lectures (там же чекер на х-е) позволяет понять, как примерно будет выглядеть обещанное Воеводским счастье ("his vision of a foundational system for mathematics in which the basic objects are homotopy types, based on a type theory satisfying the univalence axiom, and formalized in a computer proof assistant")

Идея заключается в том, чтобы усилить identity type так, чтобы больше вещей можно было доказать "в одно действие" через аналог идрисовского replace (названный в лекциях subst):

replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

Для этого из гомосексуальных гомологических примитивов собирается тип Path X a b, играющий роль {X} -> (a: X) = (b: X), который можно населить:

- "рефлом", т.е. 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 anders
notEquiv тут как раз доказательство изоморфизма. Ну и понятно что заменяются не все вхождения Bool, а "все вхождения в позициях, отмеченных Х". Любопытно, что код ничего не знает о том как обходить списки - у нас нету fmap для eats :)

Дебильные комментарии, комментарии "практиков" и школьников - как обычно, скринятся. RTFM, do you homework, пиши развёрнуто и конструктивно! https://t.me/groupoid (но там банхаммер, так что лучше сюда)
СсылкаОтветить