May. 22nd, 2017

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

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

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

Profile

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

September 2017

S M T W T F S
      1 2
3 4 5 6 7 8 9
1011 12 13 14 1516
1718 19 20212223
24252627282930

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 21st, 2017 05:39 pm
Powered by Dreamwidth Studios