Inferência de Tipos

A inferência de tipos reconstrói automaticamente os tipos de expressões, permitindo que os programadores omitam anotações enquanto o compilador calcula uma tipagem mais geral.

Definition

A inferência de tipos (reconstrução de tipos) é o processo de deduzir um tipo válido e mais geral para uma expressão a partir de sua estrutura e uso, sem exigir que o programador forneça todas as anotações de tipo.

Scope

Este tópico abrange algoritmos e teoria para inferir tipos sem anotações explícitas, centrado no sistema Hindley-Milner e no Algoritmo W com seu uso de unificação e polimorfismo let. Aborda tipos principais, decidibilidade e complexidade, e as dificuldades de estender a inferência a sistemas mais ricos com subtipagem, polimorfismo de ordem superior ou tipos dependentes.

Core questions

• Como um compilador pode reconstruir tipos quando nenhum é explicitamente escrito?
• O que é um tipo principal e quando ele sempre existe?
• Como a unificação impulsiona a inferência Hindley-Milner?
• Por que a inferência se torna indecidível ou incompleta em sistemas de tipos mais ricos?

Key theories

Inferência de tipos Hindley-Milner

A disciplina de tipos polimórficos de Milner, com o Algoritmo W, infere tipos para um cálculo lambda com polimorfismo let-bound usando unificação, formando a base da inferência em linguagens da família ML.

Esquemas de tipos principais

Damas e Milner provaram que toda expressão tipável possui um esquema de tipo principal, o tipo mais geral do qual todos os seus tipos válidos são instâncias, e que o Algoritmo W o calcula.

Tipos principais em lógica combinatória

Hindley estabeleceu a existência de tipos principais para termos tipáveis, um resultado antecedente que fundamenta a inferência de tipos em linguagens de programação posteriores.

Clinical relevance

A inferência de tipos torna as linguagens estaticamente tipadas muito mais convenientes, removendo a carga de anotações, preservando a segurança, e impulsiona recursos modernos de editores como dicas de tipo e autocompletar. Seus limites em sistemas expressivos moldam onde os programadores ainda devem fornecer anotações.

History

O trabalho de Hindley de 1969 sobre tipos principais em lógica combinatória antecipou a inferência prática. O artigo de Milner de 1978 introduziu o sistema de tipos polimórficos e o Algoritmo W para ML, e o artigo de Damas e Milner de 1982 provou a principalidade. O sistema Hindley-Milner tornou-se o padrão para ML, Haskell e muitas linguagens posteriores, com pesquisas contínuas estendendo a inferência a contextos mais ricos.

Debates

O quanto inferir versus anotar

À medida que os sistemas de tipos se tornam mais expressivos, a inferência completa torna-se indecidível, provocando debate sobre o quanto deve ser inferido automaticamente versus exigido como anotações explícitas para manter a inferência tratável e previsível.

Key figures

• Robin Milner
• Luis Damas
• Roger Hindley
• Benjamin Pierce

Seminal works

• milner1978
• damas1982
• hindley1969
• pierce2002

Frequently asked questions

O que é um tipo principal?

Um tipo principal é o tipo mais geral de uma expressão, de tal forma que qualquer outro tipo válido para essa expressão é uma instância de substituição dele; a inferência Hindley-Milner sempre calcula um tipo principal quando ele existe.

Por que nem todos os sistemas de tipos podem inferir tipos automaticamente?

A inferência depende de restrições solúveis; em sistemas expressivos, como aqueles com tipos de ordem superior ou dependentes, a inferência completa torna-se indecidível, portanto, algumas anotações devem ser fornecidas pelo programador.