I will let Maxatar responds if he wants to but I will note that his response makes much more sense to me than yours as someone who uses traditional programming language and used to do a little math a couple decades ago.
With yours, it seems that we could even equate string to int.
How can a subtype of the integer type, defined extensionally, be equal to Unit? That really doesn't make any sense to me.
> it is consistent to add `ℕ = ℤ` as an axiom
Do you have a link to this? I am unaware of this. Not saying you're wrong but I would like to explore this. Seems very strange to me.
As he explained, an isomorphism does not mean equality for all I know. cf. Cantor. How would anything typecheck otherwise? In denotational semantics, this is not how it works.
You could look into semantic subtyping with set theoretic types for instance.
type Nine int = {9} defines a subtype of int called Nine that refers to the value 9.
All variables declared of that type are initialized as containing int(9). They are equal to Nine.
If you erased everything and replaced by Unit {} it would not work. This is a whole other type/value.
How would one be able to implement runtime reflection then?
I do understand that his response to you was a bit abrupt. Not sure he was factually wrong about the technical side though. Your knee-jerk response makes sense even if it is too bad it risks making the conversation less interesting.
Usually types are defined intensionally, e.g. by name. Not by listing a set of members (extensional encoding) in their set-theoretic semantic. So maybe you have not encountered such treatment in the languages you are used to?
edit: the only way I can understand your answer is if you are only considering the Universe of types as a standalone from the Universe of values. In that universe, we only deal with types and types structured as composites in what you are familiar of perhaps?
Maybe then it is just that this Universe as formalized is insufficiently constrained/ underspecified/ over-abstracted?
It shouldn't be too difficult to define specific extensional types on top, of which singleton types would not have their extensional definitions erased.
With yours, it seems that we could even equate string to int.
How can a subtype of the integer type, defined extensionally, be equal to Unit? That really doesn't make any sense to me.
> it is consistent to add `ℕ = ℤ` as an axiom Do you have a link to this? I am unaware of this. Not saying you're wrong but I would like to explore this. Seems very strange to me.
As he explained, an isomorphism does not mean equality for all I know. cf. Cantor. How would anything typecheck otherwise? In denotational semantics, this is not how it works. You could look into semantic subtyping with set theoretic types for instance.
type Nine int = {9} defines a subtype of int called Nine that refers to the value 9. All variables declared of that type are initialized as containing int(9). They are equal to Nine. If you erased everything and replaced by Unit {} it would not work. This is a whole other type/value.
How would one be able to implement runtime reflection then?
I do understand that his response to you was a bit abrupt. Not sure he was factually wrong about the technical side though. Your knee-jerk response makes sense even if it is too bad it risks making the conversation less interesting.
Usually types are defined intensionally, e.g. by name. Not by listing a set of members (extensional encoding) in their set-theoretic semantic. So maybe you have not encountered such treatment in the languages you are used to?
edit: the only way I can understand your answer is if you are only considering the Universe of types as a standalone from the Universe of values. In that universe, we only deal with types and types structured as composites in what you are familiar of perhaps? Maybe then it is just that this Universe as formalized is insufficiently constrained/ underspecified/ over-abstracted?
It shouldn't be too difficult to define specific extensional types on top, of which singleton types would not have their extensional definitions erased.