[aatd86]

The predicate gets tested every time we do type checking? It is part of the type identity. And it is a dependent type. Just like an array type is a dependent type, the actual array type depending on the length value argument.

edit: I think I am starting to understand. In the implementations that are currently existing, Singleton types may be abstracted. My point is exactly to unabstract them so that the value is part of their identity.

And only then we can deal with only types i.e. everything from the same Universe.

[codebje]

> The predicate gets tested every time we do type checking? It is part of the type identity.

When does type checking happen?

I think it happens at compile time, which means the predicate is not used for anything at all at run time.

> edit: I think I am starting to understand. In the implementations that are currently existing, Singleton types may be abstracted. My point is exactly to unabstract them so that the value is part of their identity.

I am not sure what you mean by "to unabstract them so that the value is part of their identity", sorry. Could you please explain it for me?

> And only then we can deal with only types i.e. everything from the same Universe.

If you mean avoiding the hierarchy of universes that many dependently typed languages have, the reason they have those is that treating all types as being in the same universe leads to a paradox ("the type of all types" contains itself and that gets weird - not impossible, just weird).

[aatd86]

> the predicate is not used for anything at all at run time.

It is used for its value when declaring a new variable of a given type at runtime too. It has to be treated as a special predicate. The allocator needs to be aware of this. Runtume introspection needs to be aware of this. Parametric type instantiation also needs to know of this since it is used to create dependent types.

The point is that in the universe of types that seems to be built in dependent types, singleton Types are just Types decorrelated from their set of values. So they become indistinguishable from each other, besides their name. Or so it seems that the explanation is. It is abstracted from their value. The proposal was to keep the set definition attached. What I call unabstract them.

The point is exactly to avoid mixing up universes which can lead to paradoxes. Instead of dealing with types as some sorts of values with functions over types, mixed up with functions over values which are also types and then functions of types and values to make some sort of dependent types, we keep the algebra of types about types. We just bridge values into singleton types. Also, it should allow an implementation that relies mostly on normal constrained parametricity and those singleton types. The point is that mixing values and types (as values) would exactly lead to this type of all types issue.

But again, I am not familiar enough with the dependent type implementations to know exactly what treatment they have of the issue.