Inferência de tipo - Type inference

A inferência de tipo se refere à detecção automática do tipo de uma expressão em uma linguagem formal . Isso inclui linguagens de programação e sistemas de tipos matemáticos , mas também linguagens naturais em alguns ramos da ciência da computação e linguística .

Explicação não técnica

Tipos em uma visão mais geral podem ser associados a um uso designado, sugerindo e restringindo as atividades possíveis para um objeto daquele tipo. Muitos substantivos na linguagem especificam tais usos. Por exemplo, a palavra leash indica um uso diferente da palavra linha . Chamar algo de mesa indica outra designação do que chamá-lo de lenha , embora possa ser materialmente a mesma coisa. Embora suas propriedades materiais tornem as coisas utilizáveis ​​para alguns fins, eles também estão sujeitos a designações específicas. Este é especialmente o caso em campos abstratos, ou seja, matemática e ciência da computação, onde o material é, finalmente, apenas bits ou fórmulas.

Para excluir usos indesejados, mas materialmente possíveis, o conceito de tipos é definido e aplicado em muitas variações. Na matemática, o paradoxo de Russell gerou versões iniciais da teoria dos tipos. Em linguagens de programação, os exemplos típicos são "erros de tipo", por exemplo, ordenar a um computador que some valores que não são números. Embora materialmente possível, o resultado não seria mais significativo e talvez desastroso para o processo geral.

Em uma digitação , uma expressão se opõe a um tipo. Por exemplo, , , e são todos os termos separados com o tipo de números naturais. Tradicionalmente, a expressão é seguida por dois pontos e seu tipo, como . Isso significa que o valor é do tipo . Este formulário também é usado para declarar novos nomes, por exemplo , muito parecido com a introdução de um novo personagem em uma cena pelas palavras "Detetive Decker".

Ao contrário de uma história, em que as designações se desdobram lentamente, os objetos nas linguagens formais muitas vezes precisam ser definidos com seu tipo desde o início. Além disso, se as expressões forem ambíguas, os tipos podem ser necessários para tornar explícito o uso pretendido. Por exemplo, a expressão pode ter um tipo, mas também pode ser lida como um número racional ou real ou mesmo como um texto simples.

Como consequência, programas ou provas podem ficar tão sobrecarregados com tipos que é desejável deduzi-los do contexto. Isso pode ser possível coletando os usos de expressões não digitadas (incluindo nomes indefinidos). Se, por exemplo, um nome ainda indefinido n é usado em uma expressão , pode-se concluir que n é pelo menos um número. O processo de deduzir o tipo de uma expressão e seu contexto é a inferência de tipo .

Em geral, não apenas os objetos, mas também as atividades têm tipos e podem ser introduzidos simplesmente por seu uso. Para uma história de Jornada nas Estrelas, tal atividade desconhecida poderia ser "radiante", que pelo bem do fluxo da história é apenas executada e nunca formalmente apresentada. No entanto, pode-se deduzir seu tipo (transporte) de acordo com o que acontece. Além disso, objetos e atividades podem ser construídos a partir de suas partes. Em tal cenário, a inferência de tipo não pode apenas se tornar mais complexa, mas também mais útil, pois permite coletar uma descrição completa de tudo em uma cena composta, enquanto ainda é capaz de detectar usos conflitantes ou não intencionais.

Verificação de tipo vs. inferência de tipo

Em uma digitação, uma expressão E se opõe a um tipo T, formalmente escrito como E: T. Normalmente, uma digitação só faz sentido em algum contexto, o que é omitido aqui.

Nesse cenário, as seguintes questões são de particular interesse:

  1. E: T? Nesse caso, tanto uma expressão E quanto um tipo T são fornecidos. Agora, E é realmente um T? Este cenário é conhecido como verificação de tipo .
  2. E: _? Aqui, apenas a expressão é conhecida. Se houver uma maneira de derivar um tipo para E, então concluímos a inferência de tipo .
  3. _: T? O contrário. Dado apenas um tipo, existe alguma expressão para ele ou o tipo não tem valores? Existe algum exemplo de um T?

Para o cálculo lambda simplesmente digitado , todas as três questões são decidíveis . A situação não é tão confortável quando tipos mais expressivos são permitidos.

Tipos em linguagens de programação

Tipos são um recurso presente em algumas linguagens fortemente tipadas estaticamente . Freqüentemente, é uma característica das linguagens de programação funcional em geral. Algumas linguagens que incluem inferência de tipo incluem C ++ 11 , C # (começando com a versão 3.0), Chapel , Clean , Crystal , D , F # , FreeBASIC , Go , Haskell , Java (começando com a versão 10), Julia , Kotlin , ML , Nim , OCaml , Opa , RPython , Rust , Scala , Swift , TypeScript , Vala , Dart e Visual Basic (a partir da versão 9.0). A maioria deles usa uma forma simples de inferência de tipo; o sistema de tipo Hindley-Milner pode fornecer inferência de tipo mais completa. A capacidade de inferir tipos automaticamente torna muitas tarefas de programação mais fáceis, deixando o programador livre para omitir anotações de tipo enquanto ainda permite a verificação de tipo.

Em algumas linguagens de programação, todos os valores têm um tipo de dados declarado explicitamente em tempo de compilação , limitando os valores que uma determinada expressão pode assumir em tempo de execução . Cada vez mais, a compilação just-in-time torna a distinção entre o tempo de execução e o tempo de compilação discutível. No entanto, historicamente, se o tipo de um valor é conhecido apenas em tempo de execução, essas linguagens são digitadas dinamicamente . Em outras linguagens, o tipo de uma expressão é conhecido apenas em tempo de compilação ; essas linguagens são digitadas estaticamente . Na maioria das linguagens tipadas estaticamente, os tipos de funções de entrada e saída e variáveis ​​locais normalmente devem ser fornecidos explicitamente por anotações de tipo. Por exemplo, em C :

int add_one(int x) {
    int result; /* declare integer result */

    result = x + 1;
    return result;
}

A assinatura desta definição de função,, int add_one(int x)declara que add_oneé uma função que recebe um argumento, um inteiro , e retorna um inteiro. int result;declara que a variável local resulté um inteiro. Em uma linguagem hipotética com suporte à inferência de tipo, o código pode ser escrito assim:

add_one(x) {
    var result;  /* inferred-type variable result */
    var result2; /* inferred-type variable result #2 */

    result = x + 1;
    result2 = x + 1.0;  /* this line won't work (in the proposed language) */
    return result;
}

Isso é idêntico ao modo como o código é escrito na linguagem Dart , exceto que está sujeito a algumas restrições adicionais conforme descrito abaixo. Seria possível inferir os tipos de todas as variáveis ​​em tempo de compilação. No exemplo acima, o compilador inferiria isso resulte xteria o tipo inteiro, já que a constante 1é o tipo inteiro e, portanto, essa add_oneé uma função int -> int. A variável result2não é usada de maneira legal, então não teria um tipo.

Na linguagem imaginária em que o último exemplo foi escrito, o compilador assumiria que, na ausência de informação em contrário, +pega dois inteiros e retorna um inteiro. (É assim que funciona, por exemplo, OCaml .) A partir disso, o inferenciador de tipo pode inferir que o tipo de x + 1é um inteiro, o que significa que resulté um inteiro e, portanto, o valor de retorno de add_oneé um inteiro. Da mesma forma, uma vez que +requer que ambos os argumentos sejam do mesmo tipo, xdeve ser um inteiro e, portanto, add_oneaceita um inteiro como argumento.

No entanto, na linha subsequente, o resultado2 é calculado adicionando um decimal 1.0com aritmética de ponto flutuante, causando um conflito no uso de xpara expressões inteiras e de ponto flutuante. O algoritmo de inferência de tipo correto para tal situação é conhecido desde 1958 e é conhecido como correto desde 1982. Ele revisita as inferências anteriores e usa o tipo mais geral desde o início: neste caso, o ponto flutuante. No entanto, isso pode ter implicações prejudiciais, por exemplo, usar um ponto flutuante desde o início pode introduzir problemas de precisão que não existiriam com um tipo inteiro.

Freqüentemente, no entanto, são usados ​​algoritmos de inferência de tipo degenerados que não podem retroceder e, em vez disso, gerar uma mensagem de erro em tal situação. Esse comportamento pode ser preferível, pois a inferência de tipo nem sempre pode ser neutra por meio de algoritmos, conforme ilustrado pelo problema anterior de precisão de ponto flutuante.

Um algoritmo de generalidade intermediária declara implicitamente o resultado2 como uma variável de ponto flutuante e a adição converte implicitamente xem um ponto flutuante. Isso pode estar correto se os contextos de chamada nunca fornecerem um argumento de ponto flutuante. Tal situação mostra a diferença entre a inferência de tipo , que não envolve conversão de tipo , e a conversão de tipo implícita , que força os dados para um tipo de dados diferente, geralmente sem restrições.

Finalmente, uma desvantagem significativa do algoritmo de inferência de tipo complexo é que a resolução de inferência de tipo resultante não será óbvia para humanos (principalmente por causa do retrocesso), o que pode ser prejudicial, pois o código se destina principalmente a ser compreensível para humanos.

O recente surgimento da compilação just-in-time permite abordagens híbridas em que o tipo de argumento fornecido pelos vários contextos de chamada é conhecido em tempo de compilação e pode gerar um grande número de versões compiladas da mesma função. Cada versão compilada pode então ser otimizada para um conjunto diferente de tipos. Por exemplo, a compilação JIT permite que haja pelo menos duas versões compiladas de add_one :

Uma versão que aceita uma entrada inteira e usa conversão de tipo implícita.
Uma versão que aceita um número de ponto flutuante como entrada e usa todas as instruções de ponto flutuante.

Descrição técnica

A inferência de tipo é a capacidade de deduzir automaticamente, parcial ou totalmente, o tipo de uma expressão em tempo de compilação. O compilador é freqüentemente capaz de inferir o tipo de uma variável ou a assinatura de tipo de uma função, sem que anotações de tipo explícitas tenham sido fornecidas. Em muitos casos, é possível omitir completamente as anotações de tipo de um programa se o sistema de inferência de tipo for robusto o suficiente ou o programa ou linguagem for simples o suficiente.

Para obter as informações necessárias para inferir o tipo de uma expressão, o compilador coleta essas informações como um agregado e subsequente redução das anotações de tipo fornecidas para suas subexpressões ou por meio de uma compreensão implícita do tipo de vários valores atômicos (por exemplo, verdadeiro: Bool; 42: Inteiro; 3,14159: Real; etc.). É por meio do reconhecimento da eventual redução de expressões a valores atômicos digitados implicitamente que o compilador de uma linguagem de inferência de tipo é capaz de compilar um programa completamente sem anotações de tipo.

Em formas complexas de programação e polimorfismo de ordem superior , nem sempre é possível para o compilador inferir tanto e, ocasionalmente, são necessárias anotações de tipo para desambiguação. Por exemplo, a inferência de tipo com recursão polimórfica é conhecida como indecidível. Além disso, as anotações de tipo explícito podem ser usadas para otimizar o código, forçando o compilador a usar um tipo mais específico (mais rápido / menor) do que havia inferido.

Alguns métodos para inferência de tipo baseiam-se na satisfação da restrição ou nas teorias do módulo de satisfatibilidade .

Exemplo

Como exemplo, a função Haskellmap aplica uma função a cada elemento de uma lista e pode ser definida como:

map f [] = []
map f (first:rest) = f first : map f rest

A inferência de tipo na mapfunção procede da seguinte maneira. mapé uma função de dois argumentos, portanto, seu tipo é restrito à forma a → b → c. Em Haskell, os padrões []e (first:rest)sempre correspondem às listas, então o segundo argumento deve ser um tipo de lista: b = [d]para algum tipo d. Seu primeiro argumento fé aplicado ao argumento first, que deve ter tipo d, correspondendo ao tipo no argumento da lista, portanto f :: d → e( ::significa "é do tipo") para algum tipo e. O valor de retorno de map f, finalmente, é uma lista de tudo o que fproduz, portanto [e].

Juntar as partes leva a map :: (d → e) → [d] → [e]. Nada é especial sobre as variáveis ​​de tipo, por isso pode ser renomeado como

map :: (a  b)  [a]  [b]

Acontece que este também é o tipo mais geral, uma vez que nenhuma outra restrição se aplica. Como o tipo inferido de mapé parametricamente polimórfico , o tipo dos argumentos e resultados de fnão são inferidos, mas deixados como variáveis ​​de tipo e, portanto, mappodem ser aplicados a funções e listas de vários tipos, desde que os tipos reais correspondam em cada invocação .

Algoritmo de inferência de tipo Hindley-Milner

O algoritmo usado pela primeira vez para realizar a inferência de tipo é agora informalmente denominado algoritmo de Hindley-Milner, embora o algoritmo deva ser atribuído apropriadamente a Damas e Milner.

A origem desse algoritmo é o algoritmo de inferência de tipo para o cálculo lambda simplesmente digitado que foi desenvolvido por Haskell Curry e Robert Feys em 1958. Em 1969, J. Roger Hindley estendeu seu trabalho e provou que seu algoritmo sempre inferia o tipo mais geral. Em 1978 Robin Milner , independentemente de trabalho de Hindley, fornecido um algoritmo equivalente, Algoritmo W . Em 1982, Luis Damas finalmente provou que o algoritmo de Milner é completo e o estendeu para suportar sistemas com referências polimórficas.

Efeitos colaterais do uso do tipo mais geral

Por design, a inferência de tipo, especialmente a inferência de tipo correta (retrocesso) introduzirá o uso do tipo mais geral apropriado, no entanto, isso pode ter implicações, pois os tipos mais gerais podem nem sempre ser algoritmicamente neutros, sendo os casos típicos:

  • o ponto flutuante é considerado um tipo geral de número inteiro, enquanto o ponto flutuante introduzirá problemas de precisão
  • tipos variantes / dinâmicos sendo considerados como um tipo geral de outros tipos, que irão introduzir regras de fundição e comparação que podem ser diferentes, por exemplo, tais tipos usam o operador '+' para adições numéricas e concatenações de string, mas a operação é realizada determinado dinamicamente em vez de estaticamente

Inferência de tipo para línguas naturais

Algoritmos de inferência de tipo têm sido usados ​​para analisar linguagens naturais , bem como linguagens de programação. Algoritmos de inferência de tipo também são usados ​​em alguns sistemas gramaticais de indução e gramática baseados em restrições para linguagens naturais.

Referências

links externos