Andy Melnikov (nponeccop) wrote,
Andy Melnikov
nponeccop

Categories:

Унивалентность на кубических типах

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 (но там банхаммер, так что лучше сюда)
Tags: fp, programming, до чего техника дошла
Subscribe
  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 0 comments