Каковы наиболее сильные системы известных типов, для которых вывод является решающим?

Хорошо известно, что вывод типа Хиндли-Милнера (простой тип вычисления с полиморфизмом) имеет разрешимый вывод типа: вы можете реконструировать основные типы для любых программ без каких-либо аннотаций.$\lambda$

Добавление классов типов в стиле Haskell, похоже, сохраняет эту разрешимость, но дальнейшие добавления делают вывод без аннотаций неразрешимым (семейства типов, GADT, зависимые типы, типы Rank-N, System и т. Д.)$\omega$

Я задаюсь вопросом: какова самая сильная известная система типов с полностью разрешимым выводом? Он будет лежать где-то между Хиндли-Милнером (полностью разрешимым) и зависимым типом (полностью неразрешимым). Существуют ли аспекты DT, которые могут быть добавлены, которые сохраняют разрешимость вывода? Какие исследования были проведены, чтобы увидеть, насколько далеко это можно отодвинуть?

Я понимаю, что не существует ни одной сильнейшей системы, что, вероятно, существуют бесконечные небольшие, постепенные изменения, которые можно добавить к HM, сохраняя логический вывод. Но есть, вероятно, несколько практических кандидатов систем, которые были обнаружены.

Редактировать: учитывая, что нет «самой сильной» системы, я приму ответ, который обрисовывает в общих чертах известные системы, которые расширяют Хиндли Милнера с решительным выводом. Примерами могут быть Liquid Types, Rank-2 и т. Д.

[РЕДАКТИРОВАТЬ: Вуаля несколько слов на каждом]

Существует несколько способов расширения вывода типа HM. Мой ответ основан на многих, более или менее успешных попытках реализации некоторых из них. Первый, на который я наткнулся, - это параметрический полиморфизм . Системы типов, пытающиеся расширить HM в этом направлении, стремятся к Системе F и поэтому требуют аннотаций типов. Два заметных расширения в этом направлении, с которыми я столкнулся:

• HMF, он допускает вывод типов для всех типов System-F, что означает, что вы можете иметь универсальное количественное определение "в середине" типа, их внешний вид неявно расположен в самой высокой области, как для полиморфных типов HM. В документе четко указано, что не существует четкого правила относительно того, сколько и где могут потребоваться аннотации типов. Кроме того, типы, относящиеся к Системе F, термины обычно не имеют основного типа.

• MLF - это не только расширение HM, но и расширение системы F, которое восстанавливает свойство основного типа HM путем введения некоторого ограниченного количественного определения типов. Авторы сравнивают, что MLF строго более мощный, чем HMF, и аннотации требуются только для параметров, используемых полиморфно.

Другой способ расширения HM - это изменение области ограничений.

• HM (X) параметризован по Хиндли-Милнеру в области ограничений X. В этом подходе алгоритм HM генерирует ограничения, которые отправляются в решатель домена для X. Для обычного HM решатель домена является процедурой объединения, а домен состоит из из набора терминов построить из типов и переменных типа.
  Другим примером для X могут быть ограничения, выраженные на языке арифметики Пресбургера (в этом случае вывод / проверка типов разрешаемы) или на языке арифметики Пеано (больше не разрешимы). X варьируется по спектру теорий, каждая из которых имеет свои собственные требования относительно количества и локализации необходимых аннотаций типов и варьируется от не всех до всех.

• Классы типов в Haskell также являются своего рода расширением домена ограничения путем добавления предикатов типа в форме MyClass(MyType)(это означает, что существует экземпляр MyClass для типа MyType).
  Классы типов сохраняют вывод типов, потому что они представляют собой (почти) ортогональные концепции, в которых реализуется специальный полиморфизм .
  В качестве примера возьмем символ valтипа, val :: MyClass a => aдля которого у вас могут быть экземпляры MyClass Aи MyClass Bт. Д. Когда вы ссылаетесь на этот символ в своем коде, на самом деле, поскольку вывод типа уже выполнен, компилятор может определить, какой экземпляр класса использовать. Это означает, что тип valзависит от контекста, в котором он используется. Вот почему запуск одного valоператора приводит кambiguous type error : компилятор не может вывести любой тип на основе контекста.

Для более продвинутых систем типов, таких как GADT, семейства типов, зависимые типы, System (F) и т. Д., Тип больше не является «типом», он становится сложным вычислительным объектом. Например, это означает, что два типа, которые не выглядят одинаково, не обязательно различаются. Так что равенство типов становится совсем не тривиальным.

Чтобы дать вам пример реальной сложности, давайте рассмотрим зависимый тип списка: NList a nгде aтип объектов в списке и nего длина.
Функция добавления будет иметь тип, append :: NList a n -> NList a m -> NList a (n + m)а функция zip будет zip :: NList a n -> NList b n -> NList (a, b) n.
Представь, что теперь у нас есть лямбда \a: NList t n, b: NList t m -> zip (append a b) (append b a). Здесь первый аргумент zip имеет тип, NList t (n + m)а второй тип NList t (m + n).
Почти то же самое, но если средство проверки типов не знает, что «+» коммутирует с натуральными числами, оно должно отклонить функцию, потому что (n + m) не буквально (m + n). Теперь речь идет не о выводе / проверке типов, а о доказательстве теорем.

Жидкие типы, кажется, делают некоторый зависимый типный вывод. Но, насколько я понимаю, это не совсем зависимый тип, скорее что-то вроде обычных типов HM, для которых делается дополнительный вывод для вычисления статических границ.

Надеюсь, это поможет.