I remember a Luca Cardelli paper that explores a language with "type:type" and it contains a sentence roughly expressing: "even if the type system is not satisfying as a logic, it offers interesting possibilities for programming"
I haven't read this, and I'm not a type theorist so this is kind of over my head, but my understanding is that you can have decidable dependent types if you add some constraints - see Liquid types (terrible name).
Liquid Types are more limited than "full dependent types" like Lean, Rocq, Agda or Idris. In Liquid Types you can refine your base types (Int, Bool), but you cannot refine all types. For instance, you cannot refine the function (a:Int | a > 0) -> {x:Int | x > a}. Functions are types, but are not refinable.
These restrictions make it possible to send the sub typing check to an SMT solver, and get the result in a reasonable amount of time.
One way that is very common to have decidable dependent types and avoid the paradox is to have a type hierarchy. I.e, there is not just one star but a countable series of them *_1, *_2, *_3, .... and the rule then becomes that *_i is of type *_(i+1) and that if in forall A, B A is of type *_i and B is of type *_j, forall A, B is of type type *_(max(i, j) + 1).
I'm no expert myself, but is this the same as Russell's type hierarchy theory? This is from a quick Google AI search answer:
Bertrand Russell developed type theory to avoid the paradoxes, like his own, that arose from naive set theory, which arose from the unrestricted use of predicates and collections. His solution, outlined in the 1908 article "Mathematical logic as based on the theory of types" and later expanded in Principia Mathematica (1910–1913), created a hierarchy of types to prevent self-referential paradoxes by ensuring that an entity could not be defined in terms of itself. He proposed a system where variables have specific types, and entities of a given type can only be built from entities of a lower type.
I remember a Luca Cardelli paper that explores a language with "type:type" and it contains a sentence roughly expressing: "even if the type system is not satisfying as a logic, it offers interesting possibilities for programming"
This must be why kinds (types of types) in Haskell are a separate and less powerful thing than ordinary types?
I believe it to be historically true, but Dependent Haskell might change this (https://ghc.serokell.io/dh see unification of types and kinds).
In Lean (and I believe Rocq as well), the Type of Int is Type 0, the type of Type 0 is Type 1, and so on (called universes).
They all come from this restriction.
With respect to Lean/Rocq, that's true, with the subtle difference that Rocq universes are cumulative and Lean's are not.
I suspect not, because in that case Type is not a Type itself, but a Kind.
Access is currently forbidden.
I haven't read this, and I'm not a type theorist so this is kind of over my head, but my understanding is that you can have decidable dependent types if you add some constraints - see Liquid types (terrible name).
https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/li...
Liquid Types are more limited than "full dependent types" like Lean, Rocq, Agda or Idris. In Liquid Types you can refine your base types (Int, Bool), but you cannot refine all types. For instance, you cannot refine the function (a:Int | a > 0) -> {x:Int | x > a}. Functions are types, but are not refinable.
These restrictions make it possible to send the sub typing check to an SMT solver, and get the result in a reasonable amount of time.
One way that is very common to have decidable dependent types and avoid the paradox is to have a type hierarchy. I.e, there is not just one star but a countable series of them *_1, *_2, *_3, .... and the rule then becomes that *_i is of type *_(i+1) and that if in forall A, B A is of type *_i and B is of type *_j, forall A, B is of type type *_(max(i, j) + 1).
>if in forall A, B A is of type _i and B is of type _j, forall A, B is of type type *_(max(i, j) + 1).
Minor correction: no +1 in forall
This is correct but just delays the problem. It is still impossible to type level-generic functions (i.e. functions that work for all type levels).
The basic fundamental reality that no type theory has offered is an ability to type everything
I'm no expert myself, but is this the same as Russell's type hierarchy theory? This is from a quick Google AI search answer:
Ah is that what Lean does with its type universes?
It's "kind" of over your head, eh?