3
$\begingroup$

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?

$\endgroup$
5
  • 1
    $\begingroup$ 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? $\endgroup$ – jmite Oct 12 '20 at 7:56
  • $\begingroup$ 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. $\endgroup$ – jmite Oct 12 '20 at 8:02
  • 4
    $\begingroup$ 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? $\endgroup$ – Andrej Bauer Oct 12 '20 at 9:04
  • $\begingroup$ @AndrejBauer You may want to make this an answer, because I think you have the most correct answer so far. $\endgroup$ – Pseudonym Jan 12 at 5:29
  • $\begingroup$ 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. $\endgroup$ – Peregring-lk Jan 12 at 8:49
0
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ What type would kind be then? $\endgroup$ – Lance Pollard Jan 12 at 4:46
  • $\begingroup$ The Type "Type" would be a kind. Another kind could be functions from type to type. $\endgroup$ – Samuel Yvon Jan 12 at 15:03
-1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.