Eliminate multiple name spaces

[rossberg]

Type and value identifiers currently live in separate name spaces. Since we started allowing types as members of objects and modules, this has become quite annoying, the implementation is a hack, and it starts metastasising, e.g., the syntax of imports in #452 (or pattern matching on modules more generally) would require special syntax etc.

Since we already have capitalisation conventions distinguishing these identifiers it would be easy to merge the two name spaces. The only problem are classes, which define both a type and a value. I propose to solve this as follows:

• (Re)introduce class function types class T -> U (think of them as the type of constructors)
• They are a subtype of regular functions T -> U and have the same representation (so nothing much changes in the backend)
• However, they are also a subtype of Typ U. which allows using them as a type synonym (only the type checker cares)

While slightly special, I think this solves all the problems without being very intrusive. In the type representation we would merely reintroduce the "class" mode on functions and tweak a couple of subtyping rules. The rest of the compiler should be able to pretty much ignore this mode, as the difference to regular functions is only relevant for elaborating types in the type checker, after that they are no different from other con types.

WDYT?

[nomeata]

Sounds good to me.

Out of curiosity: Besides being more specialized to the use case that we need (and maybe thus producing better error messages), how does this differ from the previously discussed type constructor kinded t k that is a subtype of t and of Typ k? The proposed class T -> U could the be expressed as kinded (T -> U) (Typ U)?

[rossberg]

Not sure I remember that discussion. Can you refresh my memory?

[nomeata]

Well, that’s essentially all there is to it. There is a type constructor kinded t k (where both t and k are types). On the value level, it is just t (hence kinded t k <: t), but it can also be used as type k (hence kinded t k <: Typ k)

So really, it’s precisely the mechanism that you describe above, just not tied to classes.

[rossberg]

Ah, I see, so that's basically a pair of a type and a value.

That would work as well, but maybe is more general than we want (and thus perhaps even weirder?). The notion of a constructor function at least is somewhat natural. Though the subtyping rule to Typ U is a hack as well.

[nomeata]

It’s essentially the hack in isolation :-)

But since the error messages will be better with less generality, and we don’t need that feature elsewhere, no need to worry about the general variant.

[matthewhammer]

WDYT?

LGTM.

Though I don't have a lot of personal context about the problem that it's addressing in the compiler, I think I understand the problem and the solution is non-intrusive and satisying enough. The connection that @nomeata identified is interesting; I vaguely recall that other discussion, but wouldn't have made the connection myself.

[crusso]

Sorry, never noticed this issue, perhaps we should get into the habbit of assigning people. I'm ok with something like this in principal, but would like to hold off until I get the implementation of open types in (real soon now).

[ggreif]

I see a lot of capitalised imports in stdlib/, along the lines of

import Hash "hash.as";

And then followed by

public type Hash = Hash.Hash;

This would issue, when resolved as proposed, would create a slight conflict there. @matthewhammer might want to comment.

[matthewhammer]

This pattern (or something like it) shows up in the Rust standard library too. I can try to look for a good example, which I don't have handy.

How would you want to avoid it, @ggreif? Specifically, what syntax or design pattern would you prefer in place of this one?

[matthewhammer]

My understanding is that, in our ontology, types and modules should live in distinct namespaces (typing contexts) since they have distinct roles and kinds in the language design and theory, respectively.

Yet, since they are often related (one within the other), and each one needs to be abbreviated in a systematic way sometimes in the same code, we often name them with common names, as with the module Hash and the type Hash in your snippet above.

What's the alternative?