Lambda the Ultimate

Yeah. That was one of the books I refer to when I said I was "reading up." :)

Sections 6.3 states:

The enter-part of a sub-pattern is a concatenation of the enter-part of the super-pattern, and the enter-part specified in the sub-pattern...

and Section 6.5 merely re-states this basic point. Chapters 7 and 9 conspicuously don't seem to user the word "enter" at all in the descriptive text, so I don't think they address the question I'm concerned with.

The question I'm concerned with is not how the enter-part of a sub-pattern is defined, but rather how the system copes with the fact that adding to a parameter list is a contravariant extension - it makes the input requirements of the sub-pattern more strict.

For example if I have two patterns:

Base: (# x: @integer enter x #)
Derived: (# y: @integer enter y #)

then I can apply them directly to compatible argument lists:

1 -> &Base
(1,2) -> &Derived

But suppose I have a pattern variable (the same issue can be set up using virtual patterns), that I've statically qualified to refer to a sub-pattern of Base:

Pat: ##Base

and I dynamically initialize it to refer to Derived:

Derived## -> Pat##

and then try to apply it to arguments:

1 -> &Pat        {option 1}
(1,2) -> &Pat    {option 2}

Then which of these two evaluations is allowed, and which yields a static/dynamic error? The first looks statically valid, since the static bound of Pat is Base, which expects one argument, but would naively seem to be a dynamic error, since it doesn't provide the second argument expected by Derived (which is what Pat dynamically refers to). The second seems to be what we want dynamically, but I can't see how the compiler could allow that to type-check statically.

The most reasonable answer I can see (and what I suspect Beta/gbeta does in practice) is that the first option is the only one allowed, and it just doesn't intialize the new members introduced in the sub-pattern. This relies on all types having a usable default value, which means the approach would not be applicable to languages that want to eliminate pervasive null references.

I've been wondering the same thing about Beta enter lists (if you can believe that), and I've never found an answer in any of the books or articles I have. For what it's worth, your post inspired me to perform a small test and it looks like your intuition was correct: Beta only allows option 1, and the variable y retains its initial default value of zero.

Thanks for doing the smart thing and just testing it empirically. :)

Cast in terms of the simpler case of virtual methods, this amounts to saying that when overriding a virtual method, it is okay to add additional parameters, so long as they have default values (whether user-defined, or a system-provided zero/null value).

The problem case, then, is when you really do want to add a required parameter when extending a virtual pattern. A simple case for this would be when extending a Graph class with nested virtual classes for Node and Edge. What if you want to add colors to nodes, or weights to edges, and you don't want to be forced to support an implicit default value?

The solution I landed on in Spark was to have the allow constructor parameters without default values to be added to a virtual class (or my language's equivalent) so long as the virtual class was "abstract" (in the sense of never being instantiated). Once a derived outer class needed to instantiate the virtual class, it would mark it as concrete, after which no further-extension could be allowed to introduce parameters without defaults.

My language had a very constrained subset of virtual classes, though, so I'm not sure whether the approach could be applied in the general case.

The problem case, then, is when you really do want to add a required parameter when extending a virtual pattern. A simple case for this would be when extending a Graph class with nested virtual classes for Node and Edge. What if you want to add colors to nodes, or weights to edges, and you don't want to be forced to support an implicit default value?

I'm having trouble imagining how it would make sense to add required parameters to the same method. In what sense is it the same method if it has different required parameters? Is this just overloading a method name for two distinct methods?

It's harder to conceive of a case where this makes sense for a virtual method, but I'd argue it makes more sense for a virtual class.

For a method, the only thing you can really do is invoke it, so extending it ways that break that interface don't really make sense. A class might also be used as a type, and not just as a constructor for instances. In some cases you might have a nested/virtual class which is baked enough to start using as a type, but not baked enough to start using to construct instances. Thus extensions that change the constructor signature might be allowable.

One could easily argue that in such cases it would be good practice to separate out the class-as-type and class-as-constructor cases (that is, use a virtual type and a factory method, respectively). I the case of my own language (a DSL) that would have been way too much language machinery to expose to my target users.

Have you looked at dependent classes yet?

I think I saw the paper when it got posted to LtU, but hadn't read it since then. Seems to be a nice generalization of multiple dispatch to apply to classes as well (and thus very interesting in the context of Beta-like languages).

I liked their rationale for switching to named argument passing for constructors, rather than positional (it avoids complexity when you inherit parameters from multiple ancestors). I also like how they pointed out that "abstract" usually means something very different between classes (is defined, but cannot be instantiated) and methods (can be invoked, but is not defined).

Their example with a Point class dependent on a Space kind of illustrates my motivation. They have to define a separate concrete Point2D type when it comes time to actually construct anything, and that type needs to define the constructor parameters (and field storage), and override inherited abstract methods for the "getters." It's a lot of boilerplate compared to what could have been a one-line definition for a non-dependent class.

If you imagine defining separate extensions for Space2D and ColorSpace (where points have colors... don't ask me why), then not only do you have to define concrete Point2D and ColorPoint classes, but if you combine the extensions you must define ColorPoint2D.

It would be so much easier if one could just add constructor parameters to a dependent class like Point and say "when constructing a point in a ColorSpace, one must provide a color parameter." Getting sound typing for that might be tricky in the general case, but for my special case it was worth it.