Type Theory With Erasure

1. Declaração do Problema

Em linguagens de programação com tipos dependentes (como Agda, Idris e Rocq), os tipos frequentemente dependem de valores. Isso cria uma ambiguidade fundamental: quais partes de um programa são computacionalmente relevantes em tempo de execução e quais podem ser eliminadas com segurança durante a compilação?

• Abordagens Atuais: Soluções existentes frequentemente dependem da Teoria de Tipos Quantitativa (QTT), que utiliza um semianel quantitativo (por exemplo, $\{0 < \omega\}$) para rastrear o uso de variáveis. Embora eficaz, a QTT introduz complexidade em relação a restrições subestruturais e linearidade. Outras abordagens utilizam "sortes fantasma" ou análise heurística de todo o programa, que podem ser frágeis e imprevisíveis para tipos dependentes complexos.
• A Lacuna: Há uma necessidade de uma formulação estrutural, modular e livre de redução para eliminação que se integre perfeitamente à metateoria padrão da teoria de tipos, suporte a extração de código e forneça uma base semântica clara, sem depender de semânticas quantitativas complexas.

2. Metodologia

Os autores propõem uma versão estrutural da teoria de tipos com eliminação, formulada como uma Teoria Algébrica Generalizada de Segunda Ordem (SOGAT).

• Distinção de Fase Sintética: Em vez de usar semianéis quantitativos, os autores codificam a eliminação como uma distinção de fase usando uma proposição sintética, denotada por # (o marcador de eliminação).
  • Um contexto $\Gamma$ é considerado "eliminado" se contiver a proposição $\#$ (ou seja, $\# \in \Gamma$).
  • Isso cria uma distinção entre o modo de execução ($\omega$) e o modo eliminado ($0$).
  • Crucialmente, $\#$ é uma proposição sem valor de verdade; ela não pode ser construída ou descarregada arbitrariamente. Atua como um marcador que permite que termos sejam coercidos entre modos.
• Mecanismo de Coerção: A teoria introduz duas coerções:
  • Eliminação ($\#$): Se um termo $a$ é do tipo $A$ em um contexto estendido por $\#$, ele pode ser coercido para um termo eliminado ($\# a : 0: A$).
  • Elevar (\): Se um termo $a$ é eliminado, ele pode ser elevado para um termo de execução sob a suposição de $\#$ (\ a : \omega: A$).
  • Estas são inversas mútuas até igualdade definicional, garantindo que termos eliminados não dependam de dados de execução.
• Formulação Modular SOGAT: A teoria é definida como uma SOGAT estendendo a Teoria de Tipos de Martin-Löf (MLTT). Isso permite que os autores aproveitem a metateoria existente para SOGATs, incluindo semântica functorial e construção de modelos via Categorias com Famílias (CwFs).

3. Contribuições Principais

A. Formulação Teórica

• Definição SOGAT: O artigo define TT0 (Teoria de Tipos com Eliminação) como uma SOGAT. Inclui tipos ($Ty$), termos ($Tm$) indexados por modos $\{0, \omega\}$, e o marcador de eliminação ($\#$).
• Fragmento Eliminado Derivado: Uma contribuição significativa é que a teoria não precisa definir explicitamente versões eliminadas de cada formador de termo (por exemplo, $\Pi_0, \Sigma_0$). Devido ao isomorfismo entre contextos com e sem $\#$, todo o fragmento eliminado é derivado automaticamente do fragmento de execução.
• Tipos Indutivos: O framework suporta tipos indutivos onde argumentos específicos (como índices) podem ser marcados como eliminados. Lida com tipos indutivos "exóticos" onde os próprios construtores podem existir apenas no modo eliminado.

B. Modelos Semânticos

• Modelo Fam(Set): Os autores constroem um modelo padrão na categoria de famílias de conjuntos ($Fam(Set)$).
  • Neste modelo, um objeto é um par $(X_0, X_1)$ onde $X_0$ representa dados eliminados e $X_1$ representa dados de execução.
  • O marcador de eliminação $\#$ é interpretado como uma "pequena proposição" (um objeto $\phi$ tal que a exponenciação por $\phi$ isola o componente base).
  • Este modelo generaliza para qualquer topos de Grothendieck equipado com uma pequena proposição.
• Universos Comprimidos: Para lidar com universos no contexto eliminado, os autores introduzem "universos comprimidos" ($\sqrt{\phi}U$). Estes são objetos $\phi$-modais que retêm a estrutura de universos padrão, mas satisfazem a condição de que suas fibras são contráteis, permitindo que existam em contextos eliminados sem carregar dados de execução.

C. Extração de Código e Corretude

• Extração para Cálculo Lambda Não Tipado: Os autores constroem um modelo que extrai programas TT0 para cálculo lambda não tipado.
  • Termos de execução mapeiam para termos lambda.
  • Termos eliminados mapeiam para o objeto terminal (efetivamente desaparecendo).
  • Contextos com variáveis eliminadas são isomorfos a contextos sem elas.
• Colagem e Relações Lógicas: Para provar corretude, eles usam colagem para construir uma relação lógica entre o modelo de extração de código e o modelo padrão de teoria de conjuntos.
  • Teorema 27 (Não-interferência): Prova que toda função eliminada é constante em tempo de execução. Se uma função recebe um argumento eliminado, sua saída não pode depender desse argumento em tempo de execução.
  • Teoremas 25 e 26: Provam canonicidade e que o código extraído rastreia a interpretação semântica.

D. Implementação

• Elaborador: Um elaborador de brinquedo foi implementado em Agda. Ele aceita uma linguagem de alto nível (semelhante a Idris/Agda com anotações 0 e @0) e elabora-a para a SOGAT central.
• Unificação de Padrões: Os autores demonstram que, como o núcleo é estrutural, algoritmos padrão de unificação de padrões podem ser reutilizados sem necessidade de verificações quantitativas complexas ou mecanismos de generalização especiais para metavariáveis eliminadas, resolvendo problemas encontrados nas implementações atuais de Agda e Idris.

4. Resultados

• Conservatividade: A teoria é provada ser conservativa sobre MLTT. Adicionar eliminação não aumenta o poder de prova da teoria de tipos; qualquer teorema provável em TT0 é provável em MLTT padrão.
• Independência: Dados eliminados são provados ser independentes de dados de execução. Um termo eliminado em um contexto $\Gamma$ corresponde unicamente a um termo eliminado no contexto "zerado" $0\Gamma$ (onde todos os modos são definidos como 0).
• Corretude da Extração: A prova de colagem confirma que o processo de extração preserva o comportamento computacional e elimina corretamente dados irrelevantes, garantindo que o código gerado seja seguro e eficiente.

5. Significado

• Clareza Estrutural: Ao afastar-se de semianéis quantitativos para uma distinção de fase sintética, o artigo fornece uma base mais limpa e modular para eliminação. Separa o conceito de eliminação do mecanismo de rastreamento de recursos.
• Orientação de Implementação: A abordagem estrutural simplifica a implementação de verificadores de tipos e elaboradores. Remove a necessidade de verificações quantitativas ad-hoc durante a unificação, potencialmente corrigindo bugs em sistemas existentes como Idris 2 e Agda.
• Fundação Semântica: O uso de topos de Grothendieck e pequenas proposições conecta eliminação à lógica categórica mais ampla, permitindo o uso de Computabilidade Sintética de Tait para provas metateóricas.
• Extensões Futuras: O framework é projetado para ser extensível, suportando trabalho futuro potencial sobre tipos de execução, múltiplas distinções de fase (para estágio/metaprogramação) e integração com Teoria de Tipos Cúbica.

Em resumo, este artigo apresenta uma abordagem rigorosa, estrutural e semanticamente fundamentada para a teoria de tipos com eliminação, oferecendo tanto garantias teóricas (conservatividade, não-interferência) quanto benefícios práticos para a implementação de compiladores e extração de código.