Это недавняя работа Пола-Андре Мельеса и Ноама Цайльбергера, которая исследует это. В частности, в статьях « Функторы» представлены системы уточнения типов и теорема двойственности Избелла для систем уточнения типов . Там также видео беседы о первом.
Я думаю, что существует много путаницы вокруг типов уточнения из-за того, что люди считают конкретные системы репрезентативными, что приводит к тому, что цели и детали этих конкретных систем связывают с общей идеей. Суть в том, что системы уточнения типов классифицируют термины, которые существуют независимо, тогда как (не уточняющие) типы, зависимые или нет, являются частью терминов. Это может звучать знакомо и, возможно, даже несколько противоречиво.
Потенциально знакомая и, возможно, противоречивая кажущаяся часть возникает, если вы просматриваете типы по типу Карри (внешне) и типы по типу Церкви (внутренне). Когда мы думаем о типах а-ля карри, мы думаем о типах как о классификации нетипизированных терминов, которые уже имеют значение. В типах а-ля Черч, единственные существующие термины - это хорошо типизированные термины, то есть ограничения типов являются частью нашего синтаксиса. Итак, я говорю, что система типов в стиле Карри на самом деле является системой уточнения типов, уточняющей нетипизированные термины, в то время как система типов в стиле Черчи не является системой уточнения типов. Это означает, что, например, мы можем думать о простом типе лямбда-исчисления как о системе уточнения типа или как о системе типа без уточнения.
Конечно, никто не говорит, что наши термины должны быть нетипизированными. Мы также могли бы применить систему уточнения типов к типизированным терминам, и исторически это был контекст, в котором возникли типы уточнения (с таким именем). Тем не менее, приложения для мягкой печати иллюстрируют нечто более похожее на ситуацию, описанную выше.
До сих пор я ничего не говорил о зависимых типах. Причина в том, что это абсолютно ортогональная проблема. Я бы сказал, что архетипически зависимые системы типов обычно представлены в церковном стиле и, следовательно, являются не системами уточнения типов, а NuPRL (на основе вычислительной теории типов , варианта наиболее архетипически зависимой теории типов, теории типов Мартина-Лёфа) это явно система уточнения типа, как я описал. Термины в NuPRL могут даже не иметь типов! Следует признать, что тот факт, что «PRL» означает «логика уточнения программы», также может быть подсказкой. С другой стороны, Типы уточнения для ML описывают систему типов уточнения, возможно, происхождение термина, который никоим образом не является системой зависимых типов.
Что касается троек Хоара, то это система уточнения типов. Они фактически используются в качестве примера системы уточнения типов в первой статье. Однако теория типов Хоара дает нечто, что можно рассматривать как систему типов без уточнения для языка, имеющего тройки Хоара.
Чтобы получить ответ о «мощи» различных систем, необходимо указать конкретную (семейство) систем (ы) зависимых типов и конкретную (семейство) систему (ы) уточняющих типов. Термин «система зависимых типов» охватывает очень широкий класс систем типов, а «системы уточнения типов» еще шире. Даже тогда термины не являются взаимоисключающими, поэтому это не будет сравнение между "системами зависимых типов" и "системами уточняющих типов". Однако, если под «системой зависимых типов» вы подразумеваете что-то вроде Coq , а для «системы типов уточнения» что-то вроде Liquid Typesтогда это довольно односторонне. Coq обычно считается достаточно мощным, чтобы справляться практически со всей математикой на практике; вы можете буквально внедрить и доказать правильность решения SMT в Coq, а затем использовать его; и очень близкий аналог к типу подмножества может быть сформулирован. (NuPRL буквально имеет типы подмножеств.) С другой стороны, решатели SMT обычно ограничиваются разрешимыми теориями, где Coq не имеет такого ограничения; и многие системы, такие как Liquid Types, имеют ограниченный и нерасширяемый язык для указания предикатов. (Конечно, под «системой зависимых типов» можно подразумевать « зависимый ML» , а под «системой уточнения типов» NuPRL [которая также является системой зависимых типов), которая в других отношениях была бы односторонней).
