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

Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

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.