May. 22nd, 2017

bamalip: (Default)
Известно, что модели теорий зависимых типов это LCCC (с вариациями в формулировках, основанных на расслоенных категориях). Вопрос в том, как правильно определять это "LCCC". Потому как в монографиях Курьена или Джеккобса это все долго и нудно. Во-первых хочется, чтобы работало с линейными типами (программирование квантовых нововведений и все такое; ну и обычные языки этой темой начали интересоваться), т.е. недекартово обобщение, во-вторых, чтобы бодро и современно, а не ещё одна монография на тыщу страниц с диаграммным поиском. А то Гротендик, конечно, молодец со своей "йогой шести операций", но там опять же нудно и долго, потому что через 1-категории, потому что в то время, когда это писалось, ничего адекватнее не было. Но сейчас замечательно. Получается сформулировать удивительно просто - это высшая кубическая замкнутая категория, тонкости только в том, в каком виде высшая и в каком смысле замкнутая, чтобы все остальное вылезало отсюда автоматом.

Сермяжная польза такая, что получается, можно получить отсюда трансляции между языками ТК и вариантов ТТ, представляя синтаксис ТТ как инициальную высшую категорию с подходящей структурой. Ну, это общие слова про модную тему, сейчас много кто здесь ведет раскопки. В качестве немедленных результатов - категория для классической SystemF, и как результат решение скандала с Хаскеллем. Немедленно получается какой-то относительно простой вариант равенства. Можно удобно в таком сеттинге формулировать то, чем я занимался в прошлом году (хотя кому это нужно). Мне интереснее, что можно продвигаться в плане юзабельного языка на чистых топосах, с одной стороны, и в плане языковых механизмов для "ad-hoc полиморфизма" без этого ужасного резолвинга инстансов тайп-классов.

Еще хотелось бы перенести обратно на категории известные доказательства нормализуемости/cut-elimination. Для мета-разбирательств с тотальностью/консистентностью, как обычно. Не уверен, что в этом присутствует большой смысл, но имеется такой жанр и мода на него тоже не утихает. Интересно, в частности, насколько безопасны сильные формы universe polymorphism-а для случая очень предикативных иерархий.

Profile

bamalip: (Default)
шерстяной ленин

July 2017

S M T W T F S
       1
2 3 4 56 7 8
9 1011 12 13 14 15
161718 19 2021 22
23 2425 26 27 2829
3031     

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 29th, 2017 11:55 am
Powered by Dreamwidth Studios