Irei estar usando letras maiusculas para tipos e minusculas para o que não é um tipo ou é desconhecido.
Funções: (x : A) -> B === ∏x:A. B, uma função que aceita x de um tipo A e retorna algo do tipo B, também chamado de abstração, a variável pode ser omitida quando ela não aparece em B A -> B.
Implicito: {x : A} -> B, uma função aonde o parametro é implicito, aka o compilador irá achar o argumento.
Módulo: (x : A, B) === Σx:A. B, um módulo aonde a esquerda x tem um tipo A e a direita algo do tipo B, também chamado de par, módulos podem ser transparentes tendo a forma de (x : A = v, B.
Condições: (A : K) && A : K, dado que A tenha um tipo K, então A tem um tipo K.
Soundness se refere a propriedade de um sistema aonde é garantido que algo com um tipo A, jamais terá um tipo B, em um sistema sound (1 : String) nunca será aceito.
Strong normalization se refere a propriedade de um sistema aonde é garantido que a execução de qualquer programa naquele sistema, sempre termine. Ou seja, em sistemas strong normalizing, a resposta do halting problem é sempre "termina".
Um sistema inconsistente aqui se refere a qualquer sistema aonde qualquer coisa pode ser provado, isso não implica que o sistema não seja "sound", exemplos de linguagens não consistentes porém sound são OCaml e Haskell.
No geral "consistencia = soundness + strong normalization", todos os problemas discutidos aqui são sistemas aonde strong normalization foi quebrada. Mesmo o System U é sound.
Também chamados de "sorts", são conjuntos de valores, aqui pode serem tratados como "tipos de tipos", Int : Type 0 o tipo do tipo Int é Type 0.
Para evitar os paradoxos gerados por conceitos como o "o tipo de um tipo é um tipo" aka Type : Type, teremos uma hierarquia de universos. Logo Type 0 : Type 1, Type 1 : Type 2 ...
O número usado para descrever o universo, será referido como level.
Esses universos são cumulativos, portanto (A : Type L) && A : Type (L + 1).
Impredicatividade é o conceito de que algo em um universo U pode se referir a algo em um universo maior. Aqui isso se reflete no tipo de um tipo, (B : Type L) && ((x : A) -> B) : Type L e (B : L) && (x : A, B) : Type L, o tipo de A não é uma condição em ambos os casos, logo A poderia estar em um universo maior aka (K + 1) e mesmo assim ambos os tipos estariam em L.
Em contrapartida um sistema predicativo teria a forma de (A : Type L) && (B : Type L) && ((x : A) -> B) : Type L e (A : Type L) && (B : L) && (x : A, B) : Type L, o tipo de A e o tipo de B precisam ser o mesmo.
Historicamente predicatividade gera problemas, em teoria de conjuntos o caso clássico é o Russel's paradox, que basicamente usa a proposição de que "o conjunto de todos os conjuntos que não incluem ele mesmo" e em teoria dos tipos o Girard's paradox, representado pelo System U-. https://www.cs.cmu.edu/~kw/scans/hurkens95tlca.pdf
Paradoxos como esses tornam sistemas inconsistentes aka qualquer coisa pode ser provada. Para evitar isso, sistemas como o System F e o CoC, permitem apenas impredicatividade no primeiro nivel, definindo o primeiro level da hierarquia como Prop : Type 0, permitindo uma forma impredicativa de funções (B : Prop) && ((x : A) -> B) : Prop e uma impredicativa (A : Type L) && (B : Type L) && ((x : A) -> B) : Type L. https://era.ed.ac.uk/bitstream/handle/1842/12487/Luo1990.Pdf
Inferencia na presença de impredicatividade também se torna mais complexo, na verdade se torna impossivel na sua versão mais geral como presente no System F, até aonde eu sei não é conhecido se inferencia para um System F predicativo pode ser completa, porém várias tecnicas de inferencia assumem predicatividade, como Hindley-Milner inference. https://www.sciencedirect.com/science/article/pii/S0168007298000475
Note que mesmo se referindo a Prop, módulos(strong existentials) não podem serem feitos impredicativos sem permitirem representar o Girard's paradox. Porém formas fracas de módulos(weak existentials) impredicativos podem ser permitidos, aonde a esquerda do módulo não pode ser acessada. https://www.microsoft.com/en-us/research/wp-content/uploads/1998/03/Types-for-Modules.pdf
Adicionalmente impredicatividade introduz problemas de decidability na presença de subtyping, como presente no System F-sub, porém eu não sei se o mesmo problema aparece na versão predicativa do sistema. http://www2.tcs.ifi.lmu.de/~abel/lehre/SS07/Typen/pierce93bounded.pdf
E mesmo em sistemas mais limitados, uma regra de subtyping presente em OCaml é a de weakening, permitindo transformar um modulo transparente em um modulo abstrato: (M : (A = Int, Int)) && (M <= (A : Prop, A)). Tal regra permite um loop a ser descrito no sistema. https://people.mpi-sws.org/~rossberg/1ml/1ml.pdf
U = (A : Type, (A = A, A -> ()) -> ());
V = (A = U, A -> ());
V <= U;
(A = U, A -> ()) <= U; // step
(A = U, A -> ()) <= (A : Type, (A = A, A -> ()) -> ()); // weakening
(A = U, A -> ()) <= (A = U, (A = A, A -> ()) -> ());
U -> () <= (A = U, A -> ()) -> ();
(A = U, A -> ()) <= U; // loopPolimorfismo impredicativo como descrito no System F, é computacionalmente muito mais poderoso que polimorfismo não predicativo, permitindo toda forma de recursão primitiva na linguágem, recursão de tipos positiva e até mesmo self interpreters. http://compilers.cs.ucla.edu/popl16/popl16-full.pdf
Para programadores também é extremamente natural afirmar "essa função funciona para qualquer tipo", coisa que não é possivel com polimorfismo predicativo, mesmo na presença de uma hierarquia de universos.
Em vez de tentar salvar impredicatividade aqui, estarei tentando argumentar que é mais fácil trazer a conveniencia da impredicatividade para sistemas predicativos e como recuperar o poder da impredicatividade.
Coq e Agda introduzem o conceito de polimorfismo de universo, tal polimorfismo em Coq e Agda podem ser visto como um truque de engenharia, permitindo o desenvolvedor descrever uma função que funciona com qualquer tipo, (L : Level) -> (A : Type L) -> A -> A.
Porém o level pode ser feito "implicito" e ser inferido na grande maior parte dos casos(talvez em todos), permitindo recuperar a conveniencia de sistemas como System F, (A : Type) -> A -> A será representado internamente como {L : Level} -> (A : Type L) -> A -> A.
As principais vantagens dessa solução é que ela é decidable, consistente, extensivel e quase que perfeitamente homogenea para o programador. Um sistema como o predicative calculus of cumulative constructions, pode muito mais facilmente ser extendido com subtyping.
Porém esse sistema ainda não é perfeitamente homogeneo. Tipos polimórifocos sobre universos, não estão na hierarquia de universo, portanto uma função f de tipo (L : Level) -> (A : Type L) -> A -> A não pode ser instanciado com o próprio tipo.
Em Agda (L : Level) -> (A : Type L) -> A -> A : Type ω aonde ω é um natural "infinito", basicamente um universo não alcancável.
Estarei especulando soluções que não tenho provas que são consistentes lógicamente, porém ainda parecem tornar o sistema mais fácil de extender e tão flexivel quanto impredicatividade.
O paper a seguir descreve o EpCCω, um calculo predicativo, aonde polimorfismo de universo pode ser apagado no caso do level estar em uma posição erasable, tal propriedade "erasability" pode ser feita implicita e inferida completamente. A hipotese do paper é que isso é consistente. E esse sistema consegue representar o System F inteiro. https://drops.dagstuhl.de/opus/volltexte/2020/13073/pdf/LIPIcs-TYPES-2019-9.pdf
Porém estarei descrevendo um sistema ainda mais geral
--------------
Level : Type 1
(A : Type L) && (B : Type L)
---------------------------------
((x : A) -> B) : Type (L[x := 0])
(A : Type L) && (B : L)
-------------------------------
(x : A, B) : Type L (L[x := 0])A principal diferença é que qualquer ocorrencia de x no level do tipo é eliminado, portanto
((L : Level) -> (A : Type L) -> A -> A) : Type 1;
(L : Level, (A : Type L, A)) : Type 1;Enquanto tal sistema parece permitir "compactar" universos, ele é diferente, ainda mantendo um total ordering sobre universos, o level do universo aqui essencialmente se torna um contador de quão profunda são as abstrações. Eu não consegui adaptar nenhuma versão do Girard's paradox.
Porém ficaria muito surpreso se tal sistema fosse consistente.
O subtyping me parece continuar sendo decidable
U = (L : Level) => (A : Type L, (A = A, A -> ()) -> ());
V = (L : Level) => (A = U L, A -> ());
V L <= U (L + 1);
(A = U L, A -> ()) <= U (L + 1); // start
(A = U L, A -> ()) <= (A : Type (L + 1), (A = A, A -> ()) -> ()); // expand
(A = U L, A -> ()) <= (A = U L, (A = A, A -> ()) -> ()); // weaken
(U L) -> () <= (A = (U L), A -> ()) -> (); // eliminate
(A = U L, A -> ()) <= U L; // contravariance
(A = U L, A -> ()) <= (A : Type L, (A = A, A -> ()) -> ()); // fails
// A : Type L, but U L : Type (L + 1)E de bonus o Type 0 é naturalmente não habitado, fazendo com que a corecursão entre o tipo de Type e o tipo de Level tenha um caso base natural.
Assumindo que a hipotese de que erasable universe polymorphism é consistente quando o level é erasable, um totality checking trivial surge, algo é total se a erasability de level polymorphism foi seguido. Recuperando assim uma versão incompleta mas extensa de "proof irrelevance".
O predicative calculus of cumulative constructions extendido com erasable universe polymorphism. Me parece um candidato muito bom para o core de uma linguagem de programação com tipos dependente e subtyping.