Apr. 17th, 2016

akuklev: (ДР Цертуса 2011)
На днях Altenkirch, Capriotti и Kraus (arxiv:1604.03799) выложили препринт о технике расширения HoTT предтипами (соответствующими в моделях нефибрантным объектам), и в особенности предтипом строгого равенства. Получившаяся теория типов имеет разрешимый тайпчекинг, и, судя по всему (доказательство разных тонких обещают скоро опубликовать в рамках диссертации Каприотти) является консервативным над HoTT. С одной стороны, так теряется одно из основных преимуществ HoTT — априорная non-evelness, т.е. “all grammatically correct properties of objects are invariant under isomorphism”. А в расширенной HoTT существуют “предсвойства”, которые вдоль изоморфизма не переносятся.

Зачем это расширение нужно? — для того, чтобы можно было определять структуры со строгим равенством, в особенности инфинитарные структуры вроде слабых (∞,1)-категорий так, как это делается в математике сейчас. С одной стороны, я не теряю надежды, что можно определить такие объекты и в полностью фибрантном расширении HoTT (включающем, однако, высшие коиндуктивные типы, чтобы можно было определить ∞-категории пользуясь подходом из “Weak ω-categories via terminal coalgebras“ Eugenia Cheng, Tom Leinster), с другой стороны расширение Альтенкирха сотоварищи нужно уже затем, чтобы отражать имеющиеся практики в математике, ну и главное, этот подход работает прямо сейчас, а не когда-нибудь, когда рак на горе свиснет и придумается правильное фибрантное расширение.

Вообще, я не верю в то, что judgemental equality в теории типов имеет семантический смысл, в частности потому что при определении теорий типов без суждений вида a ≡ b вполне можно обойтись, если использовать подход с двусторонним тайпчекингом (bi-directional typechecking), который на практике выглядит гораздо более естественным. Разумеется, задание всех правил двустороннего тайпчекинга даёт отношение “a можно подставить вместо b” на термах, и если два терма можно подставлять друг вместо друга в обе стороны, то их логично называть подстановочно равными. Однако это выглядит скорее как свойство термов, а не как свойство объектов, ими обозначаемых.

December 2016

S M T W T F S
    123
456789 10
11121314151617
18192021222324
25262728293031

Page Summary

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 19th, 2017 06:57 pm
Powered by Dreamwidth Studios