Types of types are unit types

[josh11b]

Attempt to prove the claim that typeof(Int32) is a unit type.

[zygoloid]

Can you link to this via the pull request, assuming there is a pull request for this branch already? It seems a little unusual for our design to link directly to your repo.

[josh11b]

I would like to, but I haven't found a URL that will give the latest version of the file, just the one associated with a particular commit.

[jsiek]

I wonder if "singleton types" is a better term for what is meant here.
In a programming language there is just one "unit type".
But I think you want one of these for Int32 another another for Int64.
This use matches the meaning of singleton types.

[josh11b]

You are likely correct, I'm not very familiar with common usage here, I was just using Wikipedia as the source of truth. https://en.wikipedia.org/wiki/Unit_type says:

The carrier (underlying set) associated with a unit type can be any singleton set. There is an isomorphism between any two such sets, so it is customary to talk about the unit type and ignore the details of its value.

I don't really understand the difference here between unit and singleton types though -- presumably this argument about being isomorphic applies equally well to singleton types. Is it just that you say "unit type" when you don't care about the unique value, making them the same?

I just did some searching and it appears while this matches the usage of "singleton type" in https://typesandkinds.wordpress.com/tag/singletons/, in https://en.wikipedia.org/wiki/Scala_(programming_language) "singleton type" seems to refer to a type with a single instance instead of a single value, matching https://en.wikipedia.org/wiki/Singleton_pattern instead of https://en.wikipedia.org/wiki/Singleton_(mathematics) . In the case of this document (and the Haskell case), the value is immutable and so the difference between values and instances is too small to concern us, which is an argument for making the change.

[zygoloid]

Reflecting more on this: the situation here seems exactly analogous to the argument made in #144 that numeric literals should have singleton types. In both cases, I think the argument goes like this:

We have multiple different values (eg, 1 and 1000000, or Int and Float) that are notionally related: there is some set of operations that applies to both. There exists a common type that both values inhabit. But there are also some operations that can be performed on one value but not the other -- in particular, conversion to some type that contains some of the values but not others: 1 as Int16 is valid but 1000000 as Int16 is not, Int as Integral is valid but Float as Integral is not.

I think we should have a consistent answer here, or a rationale for why we don't want a consistent answer. Either the type of the value (and not the value itself) should indicate which operations can be performed in all cases (in which case both literals and types should inhabit singleton types -- suggesting we accept both this and the broad direction of #144), or we accept that some operations can be predicated on the values of their operands, not only on their types, in which case the argument presented here does not hold.

[github-actions]

We triage inactive PRs and issues in order to make it easier to find active work. If this PR should remain active, please comment or remove the inactive label.
This PR is labeled inactive because the last activity was over 90 days ago. This PR will be closed and archived after 14 additional days without activity.

[github-actions]

We triage inactive PRs and issues in order to make it easier to find active work. If this PR should remain active or becomes active again, please reopen it.
This PR was closed and archived because there has been no new activity in the 14 days since the inactive label was added.