Можно ли использовать элементарную аффинную логику в качестве базовой системы типов практического языка программирования?

Элементарная аффинная логика - это система типов, которая охватывает класс λ-членов, которые могут быть сокращены за элементарное время Более того, термы типа EAL могут быть сокращены с использованием абстрактного фрагмента алгоритма Лэмпинга, который мне особенно интересен, поскольку я изучаю соответствующие комбинаторы взаимодействия.

Мой вопрос: как создать практический язык программирования, используя EAL в качестве базовой системы типов? То есть, какие расширения (точки фиксирования, полиморфизм, зависимые типы, типы данных и т. Д.) Могут быть внесены в базовую систему типов, не затрагивая эту характеристику, и будет ли такой язык применим на практике, или это будет как-то слишком ограничительный по причинам, которые я не знаю?

Нечто очень похожее, но с использованием легкой аффинной логики (LAL) вместо EAL, было предпринято несколько лет назад Baillot, Gaboardi и Mogbil (вы можете найти статью здесь ). Я думаю, что их работа может быть легко обобщена до EAL, которая является более либеральной системой.

Что касается особенностей такого языка, у вас изначально есть полиморфизм (EAL является ограничением линейной логики второго порядка). Насколько я знаю, никто не смотрел на зависимые типы, но я не понимаю, почему они не должны работать. Фактически, нетипизированный EAL работает так же, как и типизированный EAL, потому что его свойства нормализации не зависят от типов.

Одним из следствий этого является то, что в EAL вы можете использовать произвольную фиксированную точку типов (см., Например, этот другой документ от Baillot) и определять типы данных в естественном рекурсивном стиле (например,$\mathtt{list\ A := nil\mathrel | A\ *\ list\ A}$), наряду с менее естественным (с точки зрения программирования) определением системы F. Тем не менее, согласно приведенному выше замечанию о нетипизированной нормализации, язык программирования, основанный на EAL, всегда будет тотальным , что означает, что у вас не будет комбинатора с фиксированной точкой, а использование рекурсивных типов не так естественно, как вы ожидаете. Например, возьмите цифры Скотта: без рекурсивных определений (данных комбинатором точек фиксирования) трудно выразить что-либо, кроме операций с постоянным временем, с этим представлением целых чисел. Поэтому вам все равно нужно будет использовать церковные цифры для итерации (т.е.$\mathtt{for}$ циклы), с помощью которого вы будете подвергаться фундаментальному ограничению стратификации легких логик (что придает им свойства сложности): вы не можете выполнять итерацию функции $\mathsf{Nat}\rightarrow\mathsf{Nat}$ который сам был определен итерацией ($\mathsf{Nat}$ вот тип церковных целых чисел).

Пример: с некоторым «церковным целочисленным хакингом» можно определить в EAL $\mathsf{dbl}:\mathsf{Nat}\rightarrow\mathsf{Nat}$ такой, что $\mathsf{dbl}\ \underline{n} = \underline{2n}$ без использования итерации. Затем вы можете повторить$\mathsf{dbl}$ определить экспоненциальную функцию $\mathsf{exp}$что, однако, само по себе не может быть повторено. Поэтому любой язык программирования, основанный на EAL, должен иметь какой-то механизм, запрещающий определенные определения путем итерации; трудно представить, как такое ограничение не приведет к тому, что программисту будет неудобно. Во всяком случае, никто не запрещает вам попробовать и посмотреть, что вы можете получить!

В любом случае, если вас интересует взаимосвязь между оптимальной оценкой, EAL и легкой логикой в ​​целом, я предлагаю вам взглянуть на работы Копполы с начала до середины 2000-х годов.