Na minha busca por artigos de pesquisa sobre sistemas de tipos para linguagens imperativas, só encontro soluções para uma linguagem com referências mutáveis, mas sem estruturas de controle imperativas genuínas, como operadores compostos, loops ou condicionais.
Portanto, não está claro como uma linguagem imperativa com inferência parcial de tipo, como http://rust-lang.org, pode ser implementada.
Os artigos não mencionam tipos parametrizados, como List of a
porque os tipos parametrizados são uma extensão trivial do sistema do tipo Hindley-Milner - apenas o algoritmo de unificação deve ser estendido e o restante da inferência funciona como está. No entanto, as atribuições não podem ser adicionadas trivialmente porque surgem paradoxos; portanto, técnicas especiais, como restrição de valor de ML, devem ser aplicadas.
Você pode recomendar trabalhos ou livros descrevendo um sistema de tipos para um idioma com loops imperativos, condicionais, IO e instruções compostas?
fonte
let val x = ref 9 in while !x>0 do (print (Int.toString (!x)); x := !x-1) end
. Então, no nível de uma pergunta de pesquisa, a resposta que você está procurando é "aplicar técnicas desenvolvidas em Caml / SML, incluindo a restrição de valor"?Respostas:
Se você está procurando uma referência funcional e clara à inferência de tipos, sou um pouco parcial em relação à " Inferência de tipos no contexto " de Gundry, McBride e McKinna de 2010 , embora esse possa não ser um bom guia para implementações existentes. .
Acho que parte da resposta é que, além da restrição de valor, realmente não há muita dificuldade em adaptar a inferência do tipo Hindley-Milner a linguagens imperativas: se você define
e1; e2
como açúcar sintático para(fn _ => e2) e1
e definewhile e1 do e2
como açúcar sintático parawhiledo e1 (fn () => e2)
, ondewhiledo
é um regular função recursivatudo funcionará bem, incluindo a inferência de tipo.
Quanto à restrição de valor ser uma técnica especial, gosto da seguinte história; Tenho certeza de que peguei no Karl Crary. Considere o código a seguir, cuja restrição de valor impedirá que você escreva no ML:
Compare-o com o código a seguir, que é totalmente sem problemas:
Sabemos o que o segundo exemplo faz: ele cria duas novas células ref que contêm
NONE
, depois colocaSOME 5
a primeira (anint option ref
), depois colocaSOME "Hello"
a segunda (astring option ref
).x
x
x
Isso sugere que um comportamento "bom" do primeiro exemplo deve se comportar exatamente da mesma maneira que o segundo exemplo - instancia o lambda no nível de tipo duas vezes diferentes. A primeira vez que instanciamos , o que fará
x
comint
que sejax [int]
avaliada uma célula de referência em esperaNONE
e depoisSOME 5
. A segunda vez que instanciarx
comstring
, o que diferencia maiúsculasx [string]
para avaliar a uma ( diferente! Exploração) célula de referênciaNONE
e depoisSOME "Hello"
. Esse comportamento é "correto" (seguro para o tipo), mas definitivamente não é o que um programador esperaria, e é por isso que temos a restrição de valor no ML, para evitar que os programadores lidem com esse tipo de comportamento inesperado.fonte
e1; e2
contém um parêntese incompatível e um ponto e vírgula (que é suposto definir). Você quis dizer(fn _ => e2) e1
?A tese de doutorado de Xavier Leroy é um bom começo.
fonte
Sinto muito por não responder minha própria pergunta, mas a referência em questão é
Uma Proposta para ML Padrão , Milner, 1983
A parte 6, "Formas derivadas padrão", abrange bastante a extinção de construções imperativas. E até agora é a referência mais antiga dessas transformações amplamente óbvias que eu pude encontrar.
fonte