Линейная зависимая теория типов

Как известно, в декартово-замкнутых категориях внутренним языком является лямбда-исчисление, а в моноидальных — линейная логика. В локально декартово-замкнутых категориях появляется возможность конструировать кроме типов X -> Y также зависимые типы (x : X) -> Y(x).

Какое же свойство является аналогом локальной замкнутости для моноидальных категорий? Вот тут (http://mathoverflow.net/questions/205902/what-is-the-monoidal-equivalent-of-a-locally-cartesian-closed-category) пишут, что это моноидальная замкнутость всех Comod-категорий данной категории.

То есть, для каждого кокоммутативного комоноида X из нашей категории, категория комодулей над ним должна быть моноидально замкнутой. Что такое кокоммутативные комоноиды? Да это "классические" (в смысле без ограничения линейности) типы, т.е. объекты, для которых клонирование и забывание элементов возможно и удовлетворяет всем естественным аксиомам. И вот для таких объектов X как раз должно быть возможно строить объекты вида (x : X) -> Y(x).

thedeemon: Звучит так, будто зависимые типы не должны быть линейными?

akuklev: Не совсем. Во всех публикациях по линейным зависимым типам именно такая фигня, кроме идеи МакБрайда про то, что не нужно чтобы в (x : X) -> Y(x) тип X был классическим, а нужно, чтобы терм Y(x) “не поглощал икса”, т.е. иксом можно только “параметризовать”, но нельзя икс элиминировать. Фактически это дополнительное требование к категории (дополнительное к моноидальной замкнутости всех комоноидных категорий), что для каждого типа X существует ещё тип Ghost(X), естественным образом наделённый структурой кокоммутативного комоноида и конструктором ⧘_⧙ : X -> Ghost(X), строго-инъективным в функториальном смысле (т.е. Id-типов), но без элиминаторов (как у вселенных, что обеспечивает параметричность).

Как такое свойство выразить категорно?

Notational sketch (Linear Dependent Type Theory)

( Read more... )