Por que não usar tipos dependentes

• Tipos dependentes (type theory) incluem objetos de prova, mas o autor os considera uma estrutura desnecessária e ineficiente
• Ele estudou diretamente sistemas históricos baseados em tipos dependentes, como AUTOMATH e o sistema formal de Martin-Löf, mas o Isabelle evoluiu como um framework lógico genérico
• O Isabelle/HOL, baseado em teoria dos tipos simples (higher-order logic), se destaca em automação, bibliotecas de grande escala e legibilidade
• Por meio do projeto ALEXANDRIA, foi demonstrado que, mesmo só com lógica de ordem superior, é possível fazer a formalização de teoremas matemáticos avançados
• Apesar da maturidade de sistemas de tipos dependentes como o Lean, o autor ainda prefere a praticidade da abordagem com lógica de ordem superior por causa de problemas de desempenho e complexidade

---

Tipos dependentes e objetos de prova

• Na teoria dos tipos dependentes, objetos de prova (proof objects) são essenciais, mas o autor os vê como desperdício de espaço
  • Na arquitetura LCF, só é possível executar etapas de prova válidas por meio de verificação de tipos no nível da linguagem de implementação, e não dentro da própria lógica
  • A percepção de Robin Milner levou à introdução do conceito de proof kernel, que se tornou a base do Isabelle
• Ao ser questionado por que “não usou tipos dependentes”, o autor responde: “usei por muito tempo”

Experiência com AUTOMATH

• Em 1977, no Caltech, ele assistiu a uma aula de N. G. de Bruijn sobre o AUTOMATH, mas não conseguiu usar o sistema diretamente
  • Na época, o sistema da Universidade de Eindhoven não estava conectado à ARPAnet e era necessário um computador baseado em ALGOL 60
• O AUTOMATH é um sistema de tipos dependentes, mas não implementa a correspondência Curry–Howard
  • O usuário precisava adicionar como axiomas os símbolos e as regras de inferência da lógica desejada
  • de Bruijn comparava isso a “um grande restaurante que oferece toda comida possível”
• O Isabelle herdou essa ideia e buscou a generalidade como framework lógico
  • Mas de Bruijn detestava teoria dos conjuntos e via a matemática como algo essencialmente baseado em tipos
• O autor questionou a verificação de correção do AUTOMATH, e de Bruijn lhe enviou um livro de teoria da linguagem (300 páginas), mas isso não o convenceu

Teoria formal de Martin-Löf

• Estudando a teoria formal de Martin-Löf na Universidade Chalmers, em Göteborg, ele ficou fascinado com a possibilidade de síntese de programas
  • Ele considerava claramente “correto” o fato de ela implementar diretamente os princípios da lógica intuicionista de Heyting
• Ele seguiu pesquisando isso por anos e implementou uma versão inicial do Isabelle com base na teoria de Martin-Löf
  • Isso ainda é incluído na distribuição atual como Isabelle/CTT
• Mas a pesquisa desmoronou por causa do ambiente dogmático centrado em Per Martin-Löf e da mudança forçada para igualdade intensional (intensional equality)
• Sistemas posteriores como Calculus of Constructions (CoC), Rocq e Lean deixaram as mesmas dúvidas
  • O CoC passou décadas acumulando várias variantes e axiomas opcionais

Escolhas de pesquisa e a direção do Isabelle

• Pesquisadores precisam escolher entre desenvolver um novo sistema formal e ampliar o uso de um já existente
  • O Isabelle foi projetado como um framework generalizado, capaz de acomodar várias lógicas
• Em 1985, Mike Gordon realizou verificação de hardware com a teoria dos tipos simples de Church
  • Depois, John Harrison criou uma codificação para dimensão de vetores
• O Isabelle/HOL acrescentou à teoria de Church classes de tipos axiomáticas e o sistema de módulos locale
• A comunidade do Lean, com base no CoC, conseguiu uma enorme formalização matemática (mathlib)

Projeto ALEXANDRIA e o teste dos limites da lógica de ordem superior

• O projeto ALEXANDRIA, apoiado pelo ERC, destacou a automação, as bibliotecas e a legibilidade do Isabelle
• No começo, esperava-se que a lógica de ordem superior tivesse limitações, mas na prática foi possível formalizar com sucesso matemática avançada, incluindo esquemas de Grothendieck
  • Paulo Emílio de Vilhena e Martin Baillon provaram que todo corpo tem uma extensão algebricamente fechada
• O projeto se expandiu até resultados avançados como o teorema de Balog–Szemerédi–Gowers
  • A afirmação de que “é impossível formalizar matemática sem tipos dependentes” desapareceu, restando apenas a de que “tipos dependentes são mais elegantes”

Lean e a visão atual sobre tipos dependentes

• O autor inveja o tamanho da comunidade do Lean e a ferramenta Blueprint, mas diz que problemas de desempenho e complexidade continuam
  • Conflitos com intensional equality e a dificuldade de decidir quando usar tipos dependentes são relatados repetidamente
• Ele compara tipos dependentes ao Full Self-Driving da Tesla, apontando expectativas excessivas e inconveniências reais

Apêndice: limites teóricos da lógica de ordem superior

• Alguns afirmam que a lógica de ordem superior é fraca do ponto de vista da teoria da prova, mas isso só significa que ela é mais fraca que a teoria dos conjuntos ZF
• Segundo os resultados do ALEXANDRIA, a lógica de ordem superior ainda consegue lidar com estruturas matemáticas complexas, como esquemas de Grothendieck
  • Apenas duas provas exigiram a adição dos axiomas ZF, e ambas tratavam de teoremas que mencionavam diretamente objetos de ZF

Nota de rodapé

• Intuicionismo é uma filosofia que vê a linguagem como mais do que um simples meio de registro, e difere da atual matemática construtiva (constructive mathematics)

[GN⁺]

Comentários do Hacker News

• Tipos dependentes são muito úteis em certas situações
  Por exemplo, seria ótimo se Python pudesse expressar e verificar por tipos algo como uma “matriz float32 de tamanho 10×5”
  Mas a ideia de identificar prova e tipo, como na correspondência de Curry–Howard, é confusa do ponto de vista humano
  Um erro de tipo parece apenas um engano corrigível, mas um erro de prova é um problema muito mais complexo e que exige raciocínio
  Por isso, vejo a verdadeira força do Lean não no sistema de tipos, mas na comunidade e na estrutura open source do mathlib
  Enquanto o AFP do Isabelle funciona como um periódico acadêmico, no Lean a colaboração baseada em pull requests é muito ativa
  Atualmente estou desenvolvendo um novo provador de teoremas, o Acorn(acornprover.org), tentando combinar as vantagens do Lean e do Isabelle
  A expressividade simples dos tipos dependentes do Lean é boa, mas, quando usada profundamente demais, fica difícil depurar

  • Em C++ ou Rust também é possível expressar esse tipo de coisa quando se trata de arrays de tamanho constante
    Só que não dá para garantir em tempo de compilação o intervalo de índices conhecido apenas em tempo de execução
    Uma linguagem genuinamente dependente pode evitar erros de runtime no nível de tipos
  • Com const generics do Rust ou non-type template parameters do C++ isso também já é bastante possível
    Na prática, mesmo em linguagens com tipos dependentes, é raro usá-los para evitar erros de runtime,
    sendo mais comum aplicá-los a invariantes de estruturas de dados ou à verificação após a definição do programa
    Referências relacionadas: division-by-zero in type theory FAQ, slides de Xavier Leroy
  • Até no TypeScript dá para imitar um pouco os tipos dependentes
    Por exemplo, como na linha 38 deste código, dá para expressar o tamanho de uma matriz no tipo
    Também implementei a definição do tipo de vetor e o tipo do resultado da multiplicação de matrizes
    Mas isso ainda é um experimento em nível de projeto pessoal e talvez não se adapte bem a projetos de dados em larga escala
  • A frase “provas são o mesmo que tipos” é interessante
    Isso está relacionado ao conceito de Propositions as Types
    Fico curioso sobre como os tipos dependentes funcionam em runtime e se são necessárias verificações de tipo tanto na compilação quanto em runtime
    Também há a dúvida se a implementação não acabaria trazendo a complexidade de muitas indireções
  • Quando alguém diz “quero expressar em Python o tipo de uma matriz 10×5”, isso no fim não quer dizer apenas que ela poderia ser definida diretamente como uma classe?

• O argumento do Dr. Paulson não é que tipos dependentes sejam ruins, mas que não são indispensáveis
  Acho que teria sido bom haver mais discussão sobre os problemas de desempenho do Lean e sobre a igualdade intencional (intensional equality)
  Casos que não são igualdade definicional, como o HEq do Isabelle(link), acabam causando problemas
  Por isso, acho melhor usar tipos dependentes o mínimo possível
  Mesmo em sistemas sem tipagem estática, como o ACL2, ainda é perfeitamente possível fazer verificação
  No fim, o importante é o equilíbrio entre praticidade e verificabilidade

  • Do ponto de vista de verificação de software, o Isabelle (não dependente) já é poderoso o suficiente
    Lean e Agda ainda são menos usados em verificação em escala industrial
    Também é interessante comparar Concrete Semantics(link) com Logical Verification 2025(link)
    Na prática, refinement types podem ser mais úteis
    Ex.: Creusot para Rust, Dafny e o exemplo de prova do leftpad em LiquidHaskell
  • Em matemática, tipos dependentes funcionam bem porque não se escreve a prova como programa
    Mas, na verificação de programas, passam a ser necessários lemas auxiliares complexos, como “duas provas são idênticas”, e isso muitas vezes não pode ser provado
  • Fico curioso sobre o motivo de dizerem que “tipos dependentes devem ser usados o mínimo possível”
  • Dizer que “não são necessários” soa como uma forma de evasão
    O importante não é se a funcionalidade é necessária para existir, e sim o quanto ela é útil
    No fim, a escolha da ferramenta é uma questão de preferência do desenvolvedor e eficiência

• É interessante como boa parte dos debates da lógica moderna acaba se reduzindo a preferências estéticas
  Se as vantagens práticas fossem realmente esmagadoras, provavelmente não haveria debate
  Como referência, o artigo de 1999 de Paulson e Lamport, “Typing in Specification Languages”, vale a leitura
  Depois disso, também evoluiu um formalismo informal como o TLA+ do Lamport

  • Eu não vejo isso como uma questão puramente estética, mas sim de trade-offs
    Em troca dos ganhos de garantias em tempo de compilação, paga-se o preço de maior complexidade e aumento no tempo de build
    A questão central é se essa troca vale a pena

• O problema do HOL (teoria de tipos simples) não é a dependência, mas a falta de força lógica
  Ele é equivalente a uma versão limitada da teoria dos conjuntos de Zermelo e é fraco demais para formalizar completamente a matemática moderna
  Em especial, é difícil lidar com problemas de tamanho em áreas como a teoria das categorias (category theory)

  • Há um caso de formalização de esquemas de Grothendieck usando o recurso de locales do Isabelle
    Fico curioso sobre o quanto isso difere do estilo real dos matemáticos
  • Para aumentar a força lógica, também é possível adicionar axiomas
    Por exemplo, ao adicionar um “inaccessible cardinal”, obtém-se algo semelhante ao conceito de “universe” na teoria de tipos

• Eu era da área de métodos formais e achava tipos dependentes incríveis, mas, na prática, usá-los era sempre uma batalha difícil
  Quando eu usava F#, tentei introduzir F*, mas os colegas acharam pesada a curva de aprendizado matemática
  No fim, cheguei à conclusão cínica de que engenheiros não aprendem bem ferramentas com matemática embutida

  • F* é menos sobre matemática e mais voltado à verificação de software, então é diferente do Lean
    Ele usa resolução de restrições baseada em SMT para permitir um uso leve de tipos dependentes
    Mas isso não responde à pergunta filosófica “isso está realmente certo?”
    O mundo das provas matemáticas e o da verificação de software são bem diferentes
  • Não é que as pessoas não queiram aprender coisas novas, e sim que julgam baixo o retorno sobre o investimento
    No fim, o tempo é limitado

• Na nossa empresa, a Phosphor, estamos experimentando combinar tipos dependentes com consultas a bancos de dados/grafos
  Isso nos permitiu contornar as limitações do RDF e criar um sistema de consultas baseado em lógica
  Na prática, estamos usando o TypeDB(typedb.com), que é mais rápido que o MongoDB e útil para modelagem de dados complexa
  Também é parecido com o conceito de ontology da Palantir

  • Fiquei curioso se poderiam explicar de forma mais concreta a frase “construir um mecanismo de crescimento não dilutivo”
  • Também queria saber por que escolheram o TypeDB e quais são os números reais de desempenho

• No fim, o segredo dos tipos dependentes parece ser saber quando não usá-los
  Em vez de criticar Lean ou Rocq, talvez em certos contextos faça sentido uma abordagem no estilo do Isabelle

• O projeto de formalização Alexandria(link) do grupo de pesquisa do Paulson é impressionante
  Em especial, o trabalho de formalização de algoritmos de computação quântica(link do artigo) é interessante

• Antes eu acreditava que tipos dependentes eram o futuro, mas, em projetos reais, a queda de produtividade era grande
  Hoje prefiro soluções mais claras e fáceis de manter
  Se a equipe consegue entender e expandir a ferramenta, então essa é a ferramenta certa

• Eu gosto mais de sistemas de tipos que ficam na fronteira dos tipos dependentes, em vez de tipos dependentes completos
  Por exemplo, o Purescript oferece por padrão row types mais poderosos que os do Haskell,
  além de listas, strings e expressões regulares no nível de tipos
  Isso pode ser usado como uma forma de programação lógica baseada em typeclasses