В поисках исследовательских работ о системах типов для императивных языков я нахожу решения только для языка с изменяемыми ссылками, но без подлинных императивных структур управления, таких как составные операторы, циклы или условные выражения.
Поэтому не ясно, как можно реализовать императивный язык с частичным выводом типа, например http://rust-lang.org .
В статьях не упоминаются параметризованные типы, например, List of a
потому что параметризованные типы являются тривиальным расширением системы типов Хиндли-Милнера - только алгоритм объединения должен быть расширен, а остальная часть вывода работает как есть. Однако назначения нельзя добавлять тривиально, поскольку возникают парадоксы, поэтому необходимо применять специальные методы, такие как ограничение значения ML.
Можете ли вы порекомендовать какие-либо статьи или книги, описывающие систему типов для языка с императивными циклами, условными выражениями, IO и составными операторами?
let val x = ref 9 in while !x>0 do (print (Int.toString (!x)); x := !x-1) end
. Итак, на уровне исследовательского вопроса, вы ищете ответ «применить методы, разработанные в Caml / SML, включая ограничение стоимости»?Ответы:
Если вы ищете аккуратную, функциональную ссылку на вывод типов, я немного неравнодушен к «Выводу типов в контексте » Гандри, МакБрайда и МакКинны 2010 года , хотя это может не быть хорошим руководством для любых существующих реализаций. ,
Я думаю, что часть ответа заключается в том, что, помимо ограничения значений, действительно нет особых трудностей в адаптации вывода типа Хиндли-Милнера к императивным языкам: если вы определяете
e1; e2
как синтаксический сахар для(fn _ => e2) e1
и определяетеwhile e1 do e2
как синтаксический сахар дляwhiledo e1 (fn () => e2)
, гдеwhiledo
регулярный рекурсивная функциятогда все будет работать нормально, включая вывод типов.
Что касается ограничения стоимости как особой техники, мне нравится следующая история; Я почти уверен, что взял это от Карла Крири. Рассмотрим следующий код, ограничение которого не позволит вам писать в ML:
Сравните это со следующим кодом, который совершенно не проблема:
Мы знаем, что делает второй пример: он создает две новые ячейки ref, содержащие
NONE
, затем вставляетSOME 5
первую (anint option ref
), а затем вставляетSOME "Hello"
вторую (astring option ref
).x
x
x
Это предполагает, что одно «хорошее» поведение первого примера состоит в том, чтобы вести себя точно так же, как ведет себя второй пример - создавать лямбду на уровне типов два разных раза. В первый раз мы создаем экземпляр
x
с помощьюint
, который приведетx [int]
к оценке для ссылки на ячейку,NONE
а затемSOME 5
. Второй раз мы создаемx
сstring
, который будет регистрx [string]
для оценки к ( разные! ) Ссылке кювете ,NONE
а затемSOME "Hello"
. Такое поведение является «правильным» (типобезопасным), но это определенно не то, чего ожидает программист, и именно поэтому у нас есть ограничение значения в ML, чтобы избежать программистов, имеющих дело с таким неожиданным поведением.источник
e1; e2
содержит несовпадающую скобку и точку с запятой (которую она должна определять). Вы имели в виду(fn _ => e2) e1
?Докторская диссертация Ксавье Леруа - хорошее начало.
источник
Я прошу прощения за то, что я ответил на свой вопрос, но ссылка на вопрос
Предложение по стандарту ML , Милнер, 1983
Часть 6 «Стандартные производные формы» довольно широко описывает десагеринг императивных конструкций. И пока это самое раннее упоминание об этих в значительной степени очевидных трансформациях, которые я смог найти.
источник