There's only one possible value of type Nine; there's only one possible value of type Unit. They're isomorphic: there's a pair of functions to convert from Nine to Unit and from Unit to Nine whose compositions are identities. Both functions are just constants that discard their argument un-inspected. "nineToUnit _ = unit" and "unitToNine _ = {9}".
You've made up your language and syntax for "type Nine int = {9}" so the rules of how it works are up to you. You're sort of talking about it like it's a refinement type, which is a type plus a predicate over values of the type. Refinement types aren't quite dependent types: they're sort of like a dependent pair where the second term is of kind Proposition, not Type; your type in Liquid Haskell would look something like 'type Nine = Int<\n -> n == 9>'.
Your type Nine carries no information, so the most reasonable runtime representation is no representation at all. Any use of the Nine boils down to pattern matching on it, and a pattern match on a Nine only has one possible branch, so you can ignore the Nine term altogether.
It is an integer. It is in the definition.
And any value should be equal to nine.
By construction Nine could have been given the same representation as int, at first. Except this is not enough to express the refinement/proposition.
One could represent it as a fat pointer with a space allocated to the set of propositions/predicates to check the value of.
That allows to check for equality for instance.
That information would not be discarded.
This is basically a subtype of int.
As such, it is both a dependent type and a refinement type. While it is true that not all refinement types are dependent types, because of cardinality.
I think Maxatar response in the same thread puts it in words that are possibly closer to the art.
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.
> 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).
> 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.
You've made up your language and syntax for "type Nine int = {9}" so the rules of how it works are up to you. You're sort of talking about it like it's a refinement type, which is a type plus a predicate over values of the type. Refinement types aren't quite dependent types: they're sort of like a dependent pair where the second term is of kind Proposition, not Type; your type in Liquid Haskell would look something like 'type Nine = Int<\n -> n == 9>'.
Your type Nine carries no information, so the most reasonable runtime representation is no representation at all. Any use of the Nine boils down to pattern matching on it, and a pattern match on a Nine only has one possible branch, so you can ignore the Nine term altogether.