Tipos Dependentes e Subestruturais

Tipos dependentes permitem que os tipos dependam de valores, possibilitando especificações precisas, enquanto tipos subestruturais, como tipos lineares e afins, controlam como os recursos são utilizados.

Definition

Tipos dependentes são tipos que dependem de valores, permitindo que propriedades precisas sejam declaradas e verificadas no nível do tipo; sistemas de tipos subestruturais restringem como as variáveis (recursos) podem ser duplicadas ou descartadas, com tipos lineares exigindo que cada uma seja usada exatamente uma vez.

Scope

Este tópico abrange disciplinas de tipagem avançadas que vão além dos sistemas convencionais: tipos dependentes, nos quais os tipos podem mencionar valores de programa, permitindo que os tipos expressem especificações completas e sirvam como provas; e tipos subestruturais (lineares, afins, de propriedade), que restringem as regras estruturais de contração e enfraquecimento para rastrear o uso de recursos, aliasing e tempos de vida. Conecta-se à correspondência de Curry-Howard e a assistentes de prova.

Core questions

• Como os tipos podem depender de valores para expressar especificações completas de programas?
• Qual é a correspondência entre tipos dependentes e provas construtivas?
• Como os tipos lineares e afins modelam recursos, propriedade e segurança de memória?
• Quais são as compensações na decidibilidade e usabilidade desses sistemas ricos?

Key theories

Teoria de tipos intuicionista (dependente)

A teoria de tipos de Martin-Löf unifica a programação e a lógica construtiva de modo que os tipos são proposições e os programas são provas, fornecendo a base para linguagens com tipos dependentes e assistentes de prova.

Lógica linear e tipos lineares

A lógica linear de Girard refina a lógica clássica e intuicionista controlando as regras estruturais, e Wadler mostrou como os tipos lineares construídos sobre ela podem gerenciar com segurança a atualização in-loco e o uso de recursos.

Estática para sistemas subestruturais

Harper desenvolve a metateoria de sistemas de tipos subestruturais e outros avançados dentro de uma estrutura uniforme de estática e dinâmica, esclarecendo sua correção e interpretação de recursos.

Clinical relevance

Tipos dependentes impulsionam assistentes de prova e software verificado, onde os programas vêm com garantias de correção verificadas por máquina. Tipos subestruturais e de propriedade sustentam linguagens de sistemas seguras para memória e concorrência, permitindo o gerenciamento manual seguro de recursos sem um coletor de lixo.

History

A teoria de tipos intuicionista de Martin-Löf (décadas de 1970-1980) estabeleceu tipos dependentes e a visão de proposições como tipos, levando a assistentes de prova como Coq, Agda e Lean. A lógica linear de Girard de 1987 introduziu o raciocínio sensível a recursos; os tipos lineares de Wadler a incorporaram ao design de linguagens, e as disciplinas de propriedade e borrow-checking posteriormente tornaram as ideias subestruturais populares na programação de sistemas.

Debates

Expressividade versus usabilidade e decidibilidade

Sistemas com tipos dependentes e subestruturais podem expressar garantias muito fortes, mas aumentam a carga sobre os programadores e podem tornar a verificação de tipos indecidível ou onerosa, impulsionando o debate sobre o quanto de poder vale o custo.

Key figures

• Per Martin-Löf
• Jean-Yves Girard
• Philip Wadler
• Robert Harper

Seminal works

• martinlof1984
• girard1987
• wadler1990
• harper2016

Frequently asked questions

O que é um tipo dependente?

Um tipo dependente é um tipo cuja definição depende de um valor, como o tipo de vetores de um comprimento específico, o que permite que o sistema de tipos imponha invariantes ricos que os tipos comuns não conseguem expressar.

O que os tipos lineares garantem?

Os tipos lineares exigem que cada valor seja usado exatamente uma vez, o que permite que um compilador permita com segurança a atualização in-loco, gerencie recursos e previna erros relacionados a aliasing sem coleta de lixo em tempo de execução.