Вывод типа для императивных операторов, отличных от присваивания

10

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

Поэтому не ясно, как можно реализовать императивный язык с частичным выводом типа, например http://rust-lang.org .

В статьях не упоминаются параметризованные типы, например, List of aпотому что параметризованные типы являются тривиальным расширением системы типов Хиндли-Милнера - только алгоритм объединения должен быть расширен, а остальная часть вывода работает как есть. Однако назначения нельзя добавлять тривиально, поскольку возникают парадоксы, поэтому необходимо применять специальные методы, такие как ограничение значения ML.

Можете ли вы порекомендовать какие-либо статьи или книги, описывающие систему типов для языка с императивными циклами, условными выражениями, IO и составными операторами?

nponeccop
источник
4
Я не уверен, что понимаю источник вашего вопроса, отчасти потому, что Standard ML на самом деле имеет составные операторы, циклы и условные выражения (пример из одной строки:) let val x = ref 9 in while !x>0 do (print (Int.toString (!x)); x := !x-1) end. Итак, на уровне исследовательского вопроса, вы ищете ответ «применить методы, разработанные в Caml / SML, включая ограничение стоимости»?
Роб Симмонс
Вопрос был в том, «какие документы о технологиях, разработанных для Caml / SML, вы рекомендуете?»
nponeccop
Хорошо, я понял это и собирался отредактировать мое последнее предложение, чтобы сказать: «Что вам нужно, чтобы найти доступную ссылку для вывода типа Хиндли-Милнера, поскольку он используется в ML?» И тогда я достиг 5-минутного лимита редактирования :-)
Роб Симмонс,

Ответы:

14

Если вы ищете аккуратную, функциональную ссылку на вывод типов, я немного неравнодушен к «Выводу типов в контексте » Гандри, МакБрайда и МакКинны 2010 года , хотя это может не быть хорошим руководством для любых существующих реализаций. ,

Я думаю, что часть ответа заключается в том, что, помимо ограничения значений, действительно нет особых трудностей в адаптации вывода типа Хиндли-Милнера к императивным языкам: если вы определяете e1; e2как синтаксический сахар для (fn _ => e2) e1и определяете while e1 do e2как синтаксический сахар для whiledo e1 (fn () => e2), где whiledoрегулярный рекурсивная функция

fun whiledo g f = if g then (f (); whiledo g f) else ();

тогда все будет работать нормально, включая вывод типов.

Что касается ограничения стоимости как особой техники, мне нравится следующая история; Я почти уверен, что взял это от Карла Крири. Рассмотрим следующий код, ограничение которого не позволит вам писать в ML:

let
   val x: 'a option ref = ref NONE
in
   (x := SOME 5; x := SOME "Hello")  
end

Сравните это со следующим кодом, который совершенно не проблема:

let
   val x: unit -> 'a option ref = fn () => ref NONE
in
   (x () := SOME 5; x () := SOME "Hello")  
end

Мы знаем, что делает второй пример: он создает две новые ячейки ref, содержащие NONE, затем вставляет SOME 5первую (an int option ref), а затем вставляет SOME "Hello"вторую (a string option ref).

xxα,ссылка(вариант(α))xΛα,ссылка[α](НИКТО)

Это предполагает, что одно «хорошее» поведение первого примера состоит в том, чтобы вести себя точно так же, как ведет себя второй пример - создавать лямбду на уровне типов два разных раза. В первый раз мы создаем экземпляр xс помощью int, который приведет x [int]к оценке для ссылки на ячейку, NONEа затем SOME 5. Второй раз мы создаем xс string, который будет регистр x [string]для оценки к ( разные! ) Ссылке кювете , NONEа затем SOME "Hello". Такое поведение является «правильным» (типобезопасным), но это определенно не то, чего ожидает программист, и именно поэтому у нас есть ограничение значения в ML, чтобы избежать программистов, имеющих дело с таким неожиданным поведением.

Роб Симмонс
источник
1
Ваша десагаредированная версия e1; e2содержит несовпадающую скобку и точку с запятой (которую она должна определять). Вы имели в виду (fn _ => e2) e1?
Tsuyoshi Ito
Правильно, Цуеши: исправлено.
Роб Симмонс
Ваш последний абзац в основном говорит: (операционная) семантика и система типов не совпадают, нужно исправить, и мы решили исправить последнее.
Раду GRIGore
Раду: конечно, я согласен с этим резюме.
Роб Симмонс
3

Докторская диссертация Ксавье Леруа - хорошее начало.

Доминик Маллиган
источник
1
Тезис не охватывает императивные циклы, условия, IO и составные операторы, не так ли? Основной причиной моего вопроса было то, что я не мог найти статьи, которые освещали бы эти темы. Документы о наборе заданий в изобилии.
nponeccop
0

Я прошу прощения за то, что я ответил на свой вопрос, но ссылка на вопрос

Предложение по стандарту ML , Милнер, 1983

Часть 6 «Стандартные производные формы» довольно широко описывает десагеринг императивных конструкций. И пока это самое раннее упоминание об этих в значительной степени очевидных трансформациях, которые я смог найти.

nponeccop
источник