Generic extensions?

[kyouko-taiga]

We have 4 generic built-in types in Hyo: Metatype, Tuple, Union, and Buffer. The compiler currently performs magic to deal with this types, in the sense that an expression Union<A, B> is processed differently than say Map<A, B>. That is all fine and well but eventually we'll want to declare extensions and conformances of these generic types, and that creates a problem.

We can already create an extension for a concrete specialization of these types. For example:

extension Int[2] { ... }

What we can't do, however, is declare an extension for all buffers. This problem is of course not limited to buffers.

One compounding problem is our implementation of generic parameters. In hc, all generic parameters are identified by their declaration. However, built-in types have no declaration. They simply "exist". So even if we could write extension Metatype { ... } we'd have no way to "name" the parameter of the type.

I found of several approaches to solve this problem and one of them was to allow extensions and conformances to declare generic parameters of their own.

extension<T, n: Int> T[n]: Deinitializable where T: Deinitializable { ... }

Now we have a way to refer to the generic parameter of Buffer, which we use in the where-clause.

I think this approach is sound but it's also relatively "expensive" in terms of complexity implementation and language complexity. One issue is that it creates new ways to express things we could already write. For example, we can already write the following extension with a where-clause specifying Key == Element:

extension<T: Hashable> Map<T, T> { ... }

My question is, therefore, whether there are other use cases that could definitely sell this feature. If not, then we can fallback on one of the other solutions I thought of. The motivation for pursuing this one is that it's the least "magic" of all.

[dabrahams]

Stupid question: why can't we just do what we do with the LLVM builtins, and wrap those builtin things in other things that have actual declarations in the standard library so they can be extended?

[dabrahams]

There is a bit of magic required to deal with these special types because it is tricky to write their representation in Hylo.

Sure, leave the magic in place. Just make Buffer<Int, 10> a wrapper for an instance of the magic type, as in: give it a private property of the magic type.

Now, the fact that we don't have variadic parameter lists is a real, but separate, issue.

[kyouko-taiga]

We can write this:

public typealias Buffer<T, n: Int> = T[n]

Then we can write extensions of Buffer just as if it had been declared as a normal type. We only need to customize name lookup a little so that it will look for extensions of Buffer when it enumerates members of Int[10].

If anyone wonders why we need the special rule, it's because normally qualified name lookup would desugar the extended type to test if it matches the lexical scope in which it is looking. But here that would always fail because we should instantiate T to Int and n to 10 before desugaring the alias.

[dabrahams]

That works, I suppose, if T[n] is not defined to be sugar for Buffer<T, n> as I expected it would be.

Your explanation at the bottom raised more questions than it answered for me. What does it mean for a type to match a lexical scope, and what does QNL do with the results of this test?

[dabrahams]

Presumably if this works for Buffer, something similar works for Tuple and Union once we have variadic generics?

[kyouko-taiga]

What does it mean for a type to match a lexical scope,

Perhaps we need to dig a little deeper into how QNL works to understand the specifics.

Nominal types have a lexical scope that is identified by their name. When we ask "what are the members of Array<Int>?", QNL translates the question as "what are the members of Array", looks in the declaration of Array, and then in all extensions that reopen this scope. Normally, for an alias, QNL first desugars the aliased type, so if we have typealias IntArray = Array<Int> and ask "what are the members of IntArray?" we'll actually ask "what are the members of Array?".

You'll notice that I said QNL searches in the declaration of Array, not Array<Int>. That's because QNL in a bound generic type is actually performed as QNL in the corresponding type constructor (Array can be understood as a type constructor (Metatype<Element>) -> Array<Element>). Then the trick is that the generic parameter of Array can be bound to a universal quantifier and we can write a formula of the form ∀x.p(x) ⇒ p(T) where p(A) means something like "Array<A> has a member named count".

Now what happens when we write typealias Buffer<T, n: Int> = T[n]? Well if we desugar Buffer we get T[n], which is a skolem. So it won't match any type because T gets bound to an existential quantifier and there is no way to prove a formula like ∃x.p(x) ⇒ p(T). Normally the skolemization isn't an issue because superfluous type parameters of a type alias should not occur in the aliased expression (e.g., typealias Useless<T> = Int). The problem manifests here because we don't have a library-level type constructor to introduce universal quantifiers. The same would happen if we wrote typealias Pair<T, U> = {T, U}.

Sadly, we can't just use universal quantification for these built-in type constructors for technical reasons. As I mentioned in the original post, generic parameters are identified by their declaration and the entire machinery to support universal quantification is based on this assumption. It is not only that we need an identity, it's also that we use this identity to locate the environment that introduces a particular parameter and figure out how we can eliminate quantifiers later on. Refactoring this machinery would be far more expensive that writing the little bit of magic that changes QNL for T[n].

Presumably if this works for Buffer, something similar works for Tuple and Union once we have variadic generics?

Yes.

[dabrahams]

When we ask "what are the members of Array?", QNL translates the question as "what are the members of Array"

Since Array is an un-qualified name, I'd expect the first question to be, “which definition of Array is found by unqualified lookup?”

QNL in a bound generic type is actually performed as QNL in the corresponding type constructor (Array can be understood as a type constructor (Metatype) -> Array).

Bringing up type constructors strikes me as needlessly complicating this discussion. I've never heard anyone speak of doing name lookup in a function (the type constructor in this case) as though the function was a scope, except where we are looking up local variables of the function. But in this case we are certainly not doing that. Why not just say it's performed as QNL in the scope of the unbound (or bound-only-by-universal-quantifiers) generic type?

Then the trick is that the generic parameter of Array can be bound to a universal quantifier and we can write a formula of the form ∀x.p(x) ⇒ p(T) where p(A) means something like "Array has a member named count".

You're losing me. Playing your example out I get

∀ x.Array<x> has a member named count ⇒ T has a member named count

What's T?

I'm trying to work my way through the rest of what you wrote but I hope you'll clarify this part first.

[kyouko-taiga]

Why not just say it's performed as QNL in the scope of the unbound (or bound-only-by-universal-quantifiers) generic type?

It is simpler indeed. Let's use that formulation.

What's T?

You are free to instantiate T to anything, thanks to universal quantification (as formally allowed by the universal-quantifier elimination rule). I think one can build an intuition by translating these in English:

• For all x, Array<x> has a member count, therefore Array<T> has a member count

This is obviously true no matter how you chose to name T. Conversely, this sentence is obviously wrong:

• There exists one x such that Array<x> has a member count, therefore Array<T> has a member count