А интуиционистская теория C*-алгебр (точнее говоря, вообще весь функан и операторные алгебры) ещё плоховато проработана, так что там пока очень много чуток разных, но эквивалентных модуло LEM вариантов, как записать сигнатурки. С вашего позволения, я пока добьюсь, чтобы обычного вещественного анализа на базе кубиков начало хватать для нужд обыкновенных численных алгоритмов (для линалга, топорного решения обыкновенных уравнений, численного интегрирования элементарных функций и стандартных диффуров, вычисления спецфункций, нахождения экстремумов, и т.д.), а уж потом это.

Но вообще вся эта штуковина будет хорошо писаться не на кубике, а на теории зависимых типов с линейными типами, а это ещё сперва сделать надо. 😉

Николай, а вы откуда и чем занимаетесь в науке?

@akuklev линейных в стиле Quantitative Type Theory достаточно?

мне приходила в голову идея о связи линейных типов и линейной алгебры, но подумалось что кроме того факта, что у обоих есть модели в моноидальных категориях, их вряд ли что-то связывает

Нет, недостаточно. Мне (пока что) представляется, что это хорошее начало, но на самом деле нас интересуют такие линейные типы, в которых естественным образом появятся спектры — линейные типы, не имеющие интуиционистского аналога.

С одной стороны, макбрайдовская идея про три типа кванторов очень похожа the way to go.

С линейными зависимыми типами есть две проблемы.

1) Что такое П-типы? Если у нас и тело функции и тип функции жрут по инстанцу аргумента, то инстанс пожрат дважды. Так нельзя.

Тут макбрайд, со своей клёвой идеей, что инстансы жрёт только аппликация на уровне термов, но не на уровне типов — она клёвая.

ну в QTT они как раз "обдумываются"

2) Что такое Id-типы? Этот вопрос — самая мякотка.

Там следует ожидать совершенно новых и интересных явлений.

Id в линейных типах не может возвращаться назад, только вперед если итерируешь по нему, или апплицируешь его.

так а что, разве линейных конструктивных логик нет?

та есть

реквестирую статьи!

Там всё достаточно плохо работает. Проблему Id-типов не решил пока никто, хотя много у кого есть понимание, что там должно бы появиться, с разных точек зрения.

Реквестировать статьи было бы хорошо, если бы они были. Пока всё вилами по воде, на уровне общих идей.

насколько я понимаю линейные типы, у нас просто вместо Var в ядре языке Stream и его комбинаторы для фьюжина (как в футарке например, может быть богатый язык доступа к этим стримам)