> 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.
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.