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.
It's sort of like having two languages in one. There is a first, interpreted language which manipulates Types and code and produces a program, and then a second language which is the program itself that ultimately gets typechecked and compiled. Typechecking in this case is not (necessarily) undecidable.
This paper is moreso about dependently-typed languages, where the type of one term can depend on the runtime value of another term.
> A function has a dependent type when the type of its result depends upon the value of its argument
Pretty straightforward, and something I'm familiar with.
> The type of all types is the type of every type, including itself.
I...don't know what this means. It's unclear to me how to understand the meaning of "the type of every type", since I don't have an intuition of how to "combine" all of those types into something that I can reason about. My first instinct would be that it's saying it's a set, but if it contains itself, doesn't that run into Russel's paradox (unless they're assuming some specific set of axioms around set construction to solve this, which seems strange to leave implicit)?
Am I missing something obvious, or is it kind of unclear what they're talking about here? Maybe my confusion is that I feel like the difference between "all" and "every" is ambiguous, so I don't know how to read this as circular other than logically grouping "all types" into one thing and "every type" into a group of separate things, only I don't know what that group even is.
5 is a value of the type Integer.
What the paper is saying, is that we can go two steps further - Integer itself is a value of the type Type, and Type itself is also a value of the type Type.
The paper uses * as a symbol (and "type of all types" as a description) designating the type Type.
>>> type(5)
<class 'int'>
>>> type(type(5))
<class 'type'>
>>> type(type(type(5)))
<class 'type'>But the solution is trivial - basically the same as the old mathematical issue "set vs class": only small types are types, large types aren't. Which types are "small"? Well, precisely those, that don't contain abstract types.
See this brilliant paper for a longer treatise (the above is the essential summary): 1ML by Andreas Rossberg
IshKebab•2mo ago
https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/li...
cjfd•2mo ago
khaledh•2mo ago
cjfd•2mo ago
IshKebab•2mo ago
cjfd•2mo ago
SkySkimmer•2mo ago
Minor correction: no +1 in forall
anon291•2mo ago
The basic fundamental reality that no type theory has offered is an ability to type everything
alcidesfonseca•2mo ago
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.
blurbleblurble•2mo ago