0
$\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$
  • 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 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 at 8:02
  • 2
    $\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 at 9:04
-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.

| cite | improve this answer | |
$\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.