AK
Вы смотрели на Cedille?
Size: a a a
2017 November 19
NK
Ну я почти формализовал кодировку юнита
ЗП
Ага, эту штуку я читал и как раз очень интересуюсь одной идеей по её части.
Тогда может напишешь Мортбергу?)
AK
А чего именно ему написать?
NK
не знаю как макс а я не смотрел, как её гуглить?
AK
Просто пока на детальную проработку этого пейпера я не нашёл с кем бы посеминарить и в какое время. По моим прикидкам, нужен семинар на 12 заседаний и минимум три докладчика, которые перемежаясь рассказывают подробно про свой кусок этой работы.
NK
какого из них? по кубику или по кодировке индуктивных типов?
AK
По кубику.
AK
Про Cedille есть черновик публикации и есть видео. Черновик слегка устаремши по сравнению с видео.
Вот черновик: http://homepage.cs.uiowa.edu/~astump/papers/cedille-draft.pdf
Вот видео: https://queuea9.wordpress.com/2017/09/02/state-of-cedille/
Вот черновик: http://homepage.cs.uiowa.edu/~astump/papers/cedille-draft.pdf
Вот видео: https://queuea9.wordpress.com/2017/09/02/state-of-cedille/
TN
Ну одно заседание я записал — свое выступление на конференции, на которую Виталия не впустили.
AK
Это внешне-типированное полиморфное лямбда-исчисление, в котором индукция для индуктивных типов выводима.
TN
Ааарон Cтемп — это смежные исследования, PTS + селф типы.
TN
Om + Fix.
AK
Внешне-типированность (_очень_) существенна, поэтому мне пока непонятно что за всем этим стоит в смысле категорной семантики. Но очень хочется понять.
AK
Есть хитрые мысли, которые хотелось бы обсудить. Но вряд ли прямо сейчас, а то мне надо полку присверлить. А то уже третьи выходные никак не присверлю, валяется прямо в коридоре. Жена съест меня скоро об неё запинаться ногами.
NK
Мы никуда не торопимся, впереди вечность
NK
Кубики интересны что там выводима не только индукция, но и унивалентность
AK
Это понятно.
AK
У нас же тоже без унивалентности совершенно никуда.