Existem duas convenções que encontrei na extensão SSReflect da Coq que parecem particularmente úteis, mas que não vi amplamente adotadas em linguagens de tipo dependente mais recentes (Lean, Agda, Idris).

Em primeiro lugar, sempre que possível, os predicados são expressos como funções de retorno booleano, em vez de tipos de dados definidos indutivamente. Isso traz a capacidade de decisão por padrão, abre mais oportunidades de prova pelo cálculo e melhora a verificação do desempenho, evitando a necessidade de o mecanismo de prova levar consigo grandes termos de prova. A principal desvantagem que vejo é a necessidade de usar lemas de reflexão para manipular esses predicados booleanos ao provar.

Em segundo lugar, os tipos de dados com invariantes são definidos como registros dependentes que contêm um tipo de dados simples mais uma prova da invariante. Por exemplo, sequências de comprimento fixo são definidas no SSReflect como:

Structure tuple_of : Type := Tuple {tval :> seq T; _ : size tval == n}.

A seq e uma prova de que o comprimento dessa sequência é um determinado valor. Isso se opõe a como, por exemplo, Idris define este tipo:

data Vect : (len : Nat) -> (elem : Type) -> Type 

Uma estrutura de dados tipicamente dependente na qual a invariante faz parte de seu tipo. Uma vantagem da abordagem do SSReflect é que ela permite a reutilização, de modo que, por exemplo, muitas das funções definidas paraseq e provas sobre eles ainda podem ser usadas comtuple (operando no subjacenteseq), enquanto que com a abordagem de Idris funcionareverse, append e similares precisam ser reescritos paraVect. O Lean realmente tem um estilo SSReflect equivalente em sua biblioteca padrão,vector, mas também tem um estilo Idrisarray que parece ter uma implementação otimizada no tempo de execução.

1Livro orientado ao SSReflect ainda reivindica oVect n A abordagem de estilo é um antipadrão:

Um antipadrão comum em linguagens de tipo dependente e o Coq em particular é codificar essas propriedades algébricas nas definições dos tipos de dados e das próprias funções (um exemplo canônico dessa abordagem são as listas indexadas por comprimento). Embora essa abordagem pareça atraente, pois demonstra o poder dos tipos dependentes de capturar certas propriedades de tipos de dados e funções neles, ela é inerentemente não escalonável, pois sempre haverá outra propriedade de interesse, que não foi prevista por um designer. do tipo de dados / função, portanto, ele terá que ser codificado como um fato externo de qualquer maneira. É por isso que defendemos a abordagem, na qual tipos de dados e funções são definidos o mais próximo possível de serem definidos por um programador, e todas as propriedades necessárias deles são provadas separadamente.

Minha pergunta é, portanto, por que essas abordagens não foram adotadas mais amplamente. Faltam algumas desvantagens ou talvez suas vantagens sejam menos significativas em idiomas com melhor suporte para correspondência de padrões dependentes do que o Coq?