# How do you have a type typed "Type" when implementing a programming language?

I am working on the base of a language model, and am wondering how to represent the base type, which is a type Type. I have heard of an "infinite chain of types", but (a) I can't seem to find it on the internet while searching anymore, and (b) I am not sure if that's what I need or what it really means in practice.

Basically, I have a system in the language like this:

type User
type String
type X
...


Internally these get compiled to something like this:

[
{
type: 'Type',
name: 'User'
},
{
type: 'Type',
name: 'String'
},
...
]


But actually, the type: 'Type' gets further compiled not pointing to the string 'Type', but to the actual Type object:

[
{
type: theTypeObject,
name: 'User'
},
{
type: theTypeObject,
name: 'String'
},
...
]


So then the problem is, I need to now define or specify the "type type" itself:

type Type


which I try represent in a similar way, so now we have:

[
{
type: 'Type',
name: 'Type'
},
...
]


which is:

let theTypeObject = { name: 'Type' }
typeTypeObject.type = theTypeObject


Is that correct? What is this really saying? It is a circular structure, does this even make sense conceptually?

What would be better to do in this situation? Or is this perfectly acceptable? Basically I would like to understand how to explain what this circular structure even means, because it just makes me confused.

The type "Type" is typed "Type". It is an element of itself...

That doesn't seem logically possible. So what should I do?

• You are saying your types are "compiled down to" something that looks like JSON. Are you working in a specific context or Programming Language (or paradigm)? Do you have subtyping or a class hierarchy? Is this a functional language? Are there dependent types? Oct 12 '20 at 7:56
• The "infinite chain of types" is something that usually comes up in dependent type theory, and it's a way to avoid the fact that if you have Type:Type then you can write an infinite loop. This is a problem if you're trying to make a type theory that is consistent as a logic, but it's not usually a problem in other contexts. So I doubt you need a chain (usually called a Universe Hierarchy), having type: type will be fine. Oct 12 '20 at 8:02
• There is nothing wrong with having a programming language with Type : Type, as long as you are aware of the fact that it might allow you to write down a non-terminating program (which you can anyhow in a Turing-complete programming langauge). The more pressing issue is: are you implementing your language in Javascript or some such? Why? Oct 12 '20 at 9:04
• @AndrejBauer You may want to make this an answer, because I think you have the most correct answer so far. Jan 12 at 5:29
• Do you need to define Type using the rules of the language itself? If a language is typed, and all objects must belong to at least one type, and types are also defined as objects, I understand that you need at least one built-in type in the machine model of the language itself. If all user-defined objects belong to a default type Typed, it makes no sense (practically, and not theoretically spoken) that such default type must be user-defined as well. Jan 12 at 8:49

I think what you might have found in your previous researches might be a pure type system.

In a pure type system, to avoid having "Type" being a "Type" at the same level that "Int" is a "Type", you would define another layer of "Types" where you would define "Type" as the entire first layer (and you would define this layer in the next one, and so on)

In practice, you could define your base types as "types", and the next layer would be kinds. The type "type" would be a kind. You might also want to consider functions of types to types as another kind.

• What type would kind be then? Jan 12 at 4:46
• The Type "Type" would be a kind. Another kind could be functions from type to type. Jan 12 at 15:03

Take the Swift language as an example. In Swift, lots of things are defined in the standard library that would be built into other languages, like Int and Double, arrays etc.

Swift has five basic types: class, struct, enum, tuple, and closure. These are built into the compiler. None of them can be used directly, but every type must be based on one of these five basic types. To describe any other type, you would possibly have an indication that it is a type, then an indication of which of the five basic types the type is based on, and then more information depending on the basic type. (A Swift compiler written in Swift would like use an enum with five cases "class", "struct", "enum", "tuple" and "closure").

You don't describe these basic types at all, you just follow the specification of the language. Of course you are free to declare a sixth basic type and call it "basictype", and create six types manually which have a basic type of "basictype", but I don't see that as being too useful.

I suspect that part of the problem might be your choice of root type.

A root type typically is a type with very few properties, because (by definition) it's the union of properties of all types. Yet a Type type, which needs to handle the complexity of your type system will have quite a few properties.

Having said that, for a language model it does not really matter what that your Type has a type that is itself Type. That's just how you model it. Models are just descriptions. But you say "compile", and that means you're actually going to do things. And that means you're dealing with such practical matters as code and data.

In particular, type systems are generally used to represent object types, where objects are combinations of code and data. Sure, there's a data property type name which has itself type String and can have a value of "Type". But that data is mostly meaningless without code.

Also, code doesn't live in its self-shaped world. Your code will not execute in an environment that already understood your type system, that's the whole point why you need code in the first place. It's your code and data which will need to materialize your type system in more primitive terms. Again, unlike a model, which can live in its own world.