3 ms·
So, let's say you have a term: 5 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 o
by wavemode 11mo ago
So, let's say you have a term: 5
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.
- saghm 11mo agoHmm okay. That makes perfect sense to me, although it still isn't something I'd get from the language they used.
- 1718627440 11mo agoIt is easy to understand in practice. For example in Python: >>> type(5) <class 'int'> >>> type(type(5)) <class 'type'> >>> type(type(type(5))) <class 'type'>