Dependent Multiplicities in Dependent Linear Type Theory

Declaração do Problema
As teorias de tipos quantitativas existentes, como a Teoria de Tipos Quantitativos (QTT) e a Teoria de Tipos Modais Graduada, permitem anotações de recursos onde variáveis possuem multiplicidades que especificam a frequência de uso. No entanto, esses sistemas geralmente dependem de multiplicidades estáticas extraídas de uma álgebra de recursos fixa (por exemplo, números naturais ou semianéis). Essa natureza estática cria limitações significativas ao lidar com lógica de programa que não representa recursos diretamente, mas os organiza, como ramificação (condicionais) e recursão.

Nos sistemas atuais, uma condição booleana usada para selecionar entre dois ramos exige que ambos os ramos consumam recursos idênticos, o que é frequentemente impraticável, já que ramos diferentes tipicamente realizam operações distintas. Da mesma forma, em funções de ordem superior ou tipos indutivos (como árvores binárias), o número de vezes que uma função é aplicada ou um recurso é consumido frequentemente depende de valores conhecidos apenas em tempo de execução (por exemplo, o número de folhas em uma árvore). Tentativas anteriores de combinar a Teoria de Tipos Dependentes (DTT) com lógica linear lutaram com a questão de se tipos que dependem de termos constituem um "uso" desses termos. Embora McBride e Atkey argumentassem que os tipos são para contemplação e não para computação (permitindo dependência de variáveis lineares), sua QTT resultante ainda restringe as multiplicidades a elementos estáticos, falhando em capturar o uso dinâmico de recursos inerente a programas recursivos e ramificação dependente de dados.

Metodologia
O artigo propõe uma nova teoria de tipos linear dependente que incorpora a lógica linear diretamente em uma Teoria de Tipos Dependentes intuicionista padrão (a "teoria hospedeira"). A inovação central é o tratamento das multiplicidades não como elementos algébricos estáticos, mas como termos dentro da própria teoria hospedeira.

1. Duas Relações de Consequência: O sistema distingue entre dois julgamentos:
   • $\vdash$: A DTT intuicionista padrão (teoria hospedeira), usada para definir tipos, termos e dependências.
   • $\Vdash$: Um cálculo consciente de recursos onde termos são derivados de "fornecimentos" (contextos lineares).
2. Fornecimentos como Tipos Intuicionistas: Diferentemente dos contextos lineares tradicionais, os fornecimentos neste sistema são termos da teoria hospedeira. Isso permite que a teoria hospedeira calcule com anotações de recursos. Especificamente, o sistema utiliza os números naturais da teoria hospedeira para definir uma "multiplicação" de fornecimentos ($\Delta \hat{m}$), onde $m$ é um termo do tipo $\mathbb{N}$. Essa operação permite que um fornecimento seja duplicado $m$ vezes, onde $m$ pode depender de outras variáveis no contexto.
3. Multiplicidades Dinâmicas: Ao permitir que a multiplicidade $m$ seja um termo aberto da teoria hospedeira, o sistema suporta anotações de recursos dinâmicas. Por exemplo, uma função mapeando sobre uma árvore pode especificar que uma função $f$ é usada exatamente leafs(t) vezes, onde leafs(t) é computado a partir da estrutura da árvore de entrada $t$.
4. Formadores de Tipo: O artigo define versões lineares dos formadores de tipo padrão da DTT (funções, pares, booleanos e tipos W) anotados com essas multiplicidades dinâmicas. Crucialmente, as regras de eliminação para booleanos e tipos W permitem que os recursos sejam distribuídos diferentemente através de ramos ou construtores com base em valores em tempo de execução.
5. Semântica: A semântica é caracterizada como "Categorias Lineares com Famílias" (lCwF), que são Categorias com Famílias (CwF) indexadas em categorias monoidais simétricas. Essa estrutura generaliza os CwFs Quantitativos usados para QTT.

Principais Contribuições

• Sintaxe com Multiplicidades Dependentes: O artigo apresenta uma sintaxe onde as multiplicidades de variáveis são termos da teoria hospedeira, permitindo a tipagem precisa de programas envolvendo ramificação e recursão que anteriormente não eram tipáveis em sistemas lineares.
• Tipos W Lineares: Um tratamento principiado de tipos indutivos (especificamente tipos W com posições finitas) em um contexto linear. O sistema fornece regras de introdução e eliminação que contabilizam corretamente o uso dinâmico de recursos de estruturas recursivas.
• Caracterização Semântica: Os autores definem lCwFs como o modelo semântico para a teoria, mostrando como modelos padrão de DTT e modelos de lógica linear se combinam. Eles demonstram que esse modelo justifica as regras intrincadas para tipos W lineares e generaliza modelos existentes para QTT.
• Realização e Apagamento: Um modelo de realização é construído (baseado em álgebras BCI) para mostrar que o fragmento intuicionista ($\vdash$) pode ser apagado para computação, deixando apenas o fragmento linear ($\Vdash$) para execução, semelhante aos fragmentos 0 e 1 da QTT.
• Implementação: A teoria é implementada em Agda. A implementação usa a interpretação semântica (mapeando julgamentos lineares para termos intuicionistas equipados com testemunhos de fornecimento) para criar um verificador de tipos rigoroso, embora ainda não prático.

Resultados

• Expressividade: O sistema tipifica com sucesso programas que exigem contagem dinâmica de recursos, como uma função map para árvores binárias onde o uso da função de mapeamento é proporcional ao número de folhas.
• Completude: O artigo prova um resultado de completude para "termos claramente lineares" (termos intuicionistas que não descartam ou duplicam valores via eliminadores específicos), mostrando que eles podem ser tipados com precisão no sistema linear.
• Recuperação da Lógica Intuicionista: Ao introduzir um comonádico exponencial linear ("!"), o sistema pode recuperar a lógica intuicionista completa dentro do fragmento linear, permitindo o uso irrestrito de recursos onde necessário.
• Compensação de Decidibilidade: Os autores reconhecem que a verificação de tipos é indecidível no caso geral, pois requer a comparação de termos abertos de números naturais (por exemplo, verificar se $\Delta \hat{m}$ é igual a $\Delta \hat{n}$). No entanto, eles observam que a igualdade proposicional na teoria hospedeira pode ser usada para convencer o verificador de tipos da equivalência de recursos.

Significado
O artigo afirma fornecer uma versão mais expressiva da Teoria de Tipos Quantitativos, migrando de álgebras de recursos estáticas para multiplicidades dinâmicas e computáveis derivadas da teoria hospedeira. Ao incorporar a lógica linear na DTT em vez de tratá-las como lógicas separadas, o sistema evita a dicotomia restritiva entre variáveis intuicionistas e lineares encontrada em trabalhos anteriores. Isso permite um "tratamento principiado consciente de recursos" de uma grande classe de tipos indutivos e funções de ordem superior. O trabalho demonstra que linguagens de tipos dependentes existentes podem ser estendidas com esse sistema, oferecendo um caminho para uma gestão de recursos mais precisa na programação funcional sem sacrificar a expressividade dos tipos dependentes. Os autores posicionam seu trabalho como uma generalização da QTT que resolve as limitações das multiplicidades estáticas no manuseio de uso de recursos dependente de tempo de execução.