Inferência de tipo para declarações imperativas que não sejam atribuição

10

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 aporque 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?

nponeccop
fonte
4
Não sei se entendi a origem da sua pergunta, em parte porque o ML padrão realmente possui operadores compostos, loops e condicionais (exemplo de uma linha:) 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"?
9118 Rob Simmons
A pergunta era "que artigos sobre as técnicas desenvolvidas para o Caml / SML você recomenda?"
Noneeccop
Ok - eu tinha descoberto isso e estava prestes a tentar editar minha última frase para dizer "O que você está procurando é uma referência acessível para a inferência do tipo Hindley-Milner, como é usada no ML?" E então eu bati o limite edição 5 minutos :-)
Rob Simmons

Respostas:

14

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; e2como açúcar sintático para (fn _ => e2) e1e define while e1 do e2como açúcar sintático para whiledo e1 (fn () => e2), onde whiledoé um regular função recursiva

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

tudo 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:

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

Compare-o com o código a seguir, que é totalmente sem problemas:

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

Sabemos o que o segundo exemplo faz: ele cria duas novas células ref que contêm NONE, depois coloca SOME 5a primeira (an int option ref), depois coloca SOME "Hello"a segunda (a string option ref).

xxα.ref(opção(α))xΛα.ref[α](NENHUM)

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á xcom intque seja x [int]avaliada uma célula de referência em espera NONEe depois SOME 5. A segunda vez que instanciar xcom string, o que diferencia maiúsculas x [string]para avaliar a uma ( diferente! Exploração) célula de referência NONEe depois SOME "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.

Rob Simmons
fonte
11
Sua versão sugerida e1; e2contém um parêntese incompatível e um ponto e vírgula (que é suposto definir). Você quis dizer (fn _ => e2) e1?
Tsuyoshi Ito
Certo, Tsuyoshi: consertado.
Rob Simmons
Seu último parágrafo diz basicamente: a semântica (operacional) e o sistema de tipos não coincidem, é preciso corrigir e escolhemos corrigi-lo.
Radu GRIGore
Radu: claro, concordo com esse resumo.
Rob Simmons
3

A tese de doutorado de Xavier Leroy é um bom começo.

Dominic Mulligan
fonte
11
A tese não cobre loops imperativos, condicionais, IO e declarações compostas, não é? O principal motivo da minha pergunta foi que não consegui encontrar documentos que abordassem esses tópicos. Trabalhos sobre digitação são abundantes.
Nponeccop
0

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.

nponeccop
fonte