Choosing an Approach to Executable Semantics

[geoffromer]

This discussion took place on our Discourse forum on April 1-2, 2020. I'm copying it here so that we have it for reference after the forum is shut down. I recommend that any further discussion take place on a separate thread, but please let me know if you see any errors I've made during copying.

@dabrahams:

Hi everybody,

I've taken a step back to think about our overall approach to this part of the project, and would love to get your input. Yes, this is a long post (sorry!). The TL;DRs among us should feel free to skip to the Proposal section.

Goals of Executable Semantics

The goals of @jsiek's executable_semantics contribution, as I understand them, are:

1. To provide a “specification for Carbon in code,” that directly expresses the language design.
2. To provide a platform for proof-of-concept feature implementations, such that an implementation might become a reasonable requirement for consideration of a formal proposal.

To me, success with those main goals implies these consequent ones:

• It will be fast and easy to digest the code related to (i.e. the specification of) any given language feature.
• It will be fast and easy to modify the code to support a new language feature—or at least any difficulty should be caused by the complexity of the feature to be implemented rather than the coding environment.
• Syntax choices should be made to simplify and clarify use-sites.
• This code should contain as little incidental complexity—details unrelated to the code's main goals—as possible. For the most part, readers and writers of this code should be able to function without worrying about safety, low-level performance, unintended state sharing in the implementation, or other subtleties.

Of course, I may not have captured the goals accurately, and there may be other important goals I've left out. I'm eager to hear other perspectives.

The Conceptual Model

The code contributed by @jsiek is built on a well-established conceptual model (“the model”) that relies heavily on recursive algebraic data types (a.k.a. dynamically polymorphic trees) and structural pattern matching. Because it expresses meaning clearly and succinctly, the model is the lingua franca of CS research, and can be expressed directly in languages such as ML and Haskell that have rich native support for those features. In languages with native support, recursive ADTs and pattern matching are considered so fundamental that they are commonly among the first features anyone learns. The upshot is that an interpreter or type checker for a small language can usually be expressed in one page of code that is understandable to even a programmer with only a basic working knowledge of the implementation language.

The Model in C++

Expressing these ideas in C++ is certainly possible. In fact, every major language implementation I've seen written in C++ uses an expression of the same basic model. Even if they were allowed to become inefficient, though, I doubt these implementations could satisfy our main goals for executable semantics, due to these properties of C++:

• Achieving safety and avoiding subtle problems requires work and code, which amounts to incidental complexity that makes code larger and harder to grasp.
• Weak support for sum types (“closed” dynamic polymorphism):
  • unions, the language's built-in sum types, are both brittle and inflexible.
  • Useful and safe abstract sum types are only supported by libraries (e.g. std::variant). As a result, they don't benefit from language features that support succinct usage and descriptive names for the types' different forms.
  • Even std::variant is not a recursive sum type, which is key to representing the trees used by the model.
  • The most expressive use of std::variant requires support components not supplied by the standard library.
• C++ has no support for dynamic pattern matching. Structured binding declarations are useful for decomposing values with statically-known structure, but in the model, the structure is dynamically polymorphic.
• “Open” dynamic polymorphism (e.g. class hierarchies) are available, but:
  • introduce incidental declaration boilerplate.
  • tend to raise issues of safety and unintended sharing that can only be nullified with more ceremony, or by giving up the clarity benefits of mutating methods where mutation is natural.
  • The virtual functions used for dispatching spread logic that is otherwise visible together across many types and functions. For example, instead of one TypeCheck function where the overall logic of the type checker is captured, we end up with distinct virtual functions for type-checking each shape of AST node. When—as is common—the code for handling any given structural pattern fits in a line or two, or one block of common code can be used to handle a range of structural patterns, I’ve found this approach frustratingly verbose, and prone to land me in an uncomfortable position where the choice is between repeating a small code fragment or factoring it out and neither one seems good for overall readability.

Aside: Limitations of classic Yacc (since overcome in recent versions of Bison) led to the initial code being implemented unsafely, with unions and pervasive mutable-pointers-to-mutable state. The issues listed above were brought to the fore during the process of unwinding that technical debt.

Interaction with Coding Conventions

C++ is an extremely flexible language, and with enough effort and hand-crafted EDSL components, one can mitigate many of the weaknesses listed in the previous section. However, the mitigations often involve advanced usage of the language that stretch conventional ideas about best practices. For example, expressively switching over std::variant requires something like this code:

// An "overloaded function object" that exposes the function call operators
// of the constituent `F`s as an overload set.
template <class... Fs>
struct Overload : Fs... {
  using Fs::operator()...;
};

// Returns the result of applying the best-matching function object in `fs` to the 
// active alternative of the `std::variant` `v`.
template <class V, class... Fs>
auto Switch(V&& v, Fs&&... fs)
    -> decltype(std::visit(Overload<Fs...>{std::forward<Fs>(fs)...},
                           std::forward<V>(v))) {
  return std::visit(Overload<Fs...>{std::forward<Fs>(fs)...}, v);
}

Aside from its complexity, this code uses inheritance as an implementation detail, without a virtual destructor, to create the overload set, which bumps up against many coding standards, including our own. In a codebase where switching over sum types is a staple, perhaps the deviation is worthwhile, but reasonable people may disagree.

As another example, sometimes code processing these trees needs to handle all the representational alternatives, but it's also very common to probe for one or two representations, and do nothing (or flag an internal error) in the other cases. When using the “open” dynamic polymorphism approach, the most direct method is to use a dynamic_cast to extract the cases of interest, which again causes friction with common coding guidelines. As with the earlier example, reasonable people can take different positions on whether it is worth violating such a guideline.

For a final example, if we take an “open polymorphism” approach, we end up with methods implementing switch cases. Convention dictates that these methods be grouped into files by the type of *this, rather than by the identity of the method. Doing that separates logic which, in its most natural expression, goes together.

These examples are by no means exhaustive; I’ve provided them just to give a sense of the challenges we face.

Proposal

It seems to me that serving the primary goals of executable semantics is going to mean exploring directions that stretch the usual boundaries of common C++ coding practices, and that it will be inefficient to discuss each possible deviation individually with the group as a whole. Also, I don’t think that PRs against the existing implementation make it easy to appreciate the possible benefits various techniques might have in the long run, because of the contrast between the amount of change needed and the small differences that can be captured in a reasonably-reviewable PR.

In order to make informed decisions about how to approach a C++ implementation, I suggest we look at an implementation of Carbon’s executable semantics written in a different language—one better-suited to the model than C++. We can use that to establish a baseline expectation (or two—perhaps exploring both open and closed dynamic polymorphism) for an optimal realization of the main goals. Then, together with all of you, I'd like to explore ways to translate it into C++ and discuss which guidelines might need bending.

There are lots of languages with the necessary features, but I’d like to use Swift for the following reasons:

• It has all the ADT and pattern-matching features needed to express the model directly.
• It’s an imperative C-family language written by C++ programmers, so it should communicate fairly well to a group with a C++ background.
• It supports first-class mutable value semantics, a key idiom of C++ programming not supported by many of the more “researchy” functional languages.
• I’m very familiar with it, so the work can go quickly.
• I already have working lexer, parser, and AST implementations.

It may sound like a big job, but so far it has been surprisingly easy to capture the functionality of the existing implementation. I feel pretty confident I could be done in a couple of weeks if I was working alone (less, with help). In fact I think this may be a faster path to a quality C++ implementation than trying to incrementally move the code we currently have, in part because we’re not yet sure which direction we need to go.

Thanks

Your feedback would be very much appreciated. Thanks for your indulgence and sorry again for the long post.

-Dave

@gribozavr:

There are lots of languages with the necessary features, but I’d like to use Swift for the following reasons:

+1, or Rust. I know that we discussed these questions before and the primary argument was that we want to minimize the number of languages, but I don't think it is such a big deal if we are talking about languages like Rust and Swift that will (I hope!) influence Carbon's design heavily. I expect active contributors to be at least familiar with Rust and Swift (and probably other languages) just to be able to make and evaluate Carbon proposals.

@dabrahams:

FWIW, I'd be just as happy from a “Dave is having fun and enjoying programming” point-of-view to do it in Rust, but from a “what is going to make this process efficient under a tight schedule” point-of-view, it doesn't seem like a good idea. I'd have to start over, find some kind of Bison for Rust, and scale enough of Rust's learning curve to be able to write not just a working program, but an expressive one.

@geoffromer:

I'm not entirely clear on what actionable new information we should expect a Swift implementation to give us, since most of the problems we're struggling with are already solved in Swift (e.g. straightforward support for ADTs and pattern matching). The one exception I can think of is the question of open vs. closed polymorphism, but there I think the main issue is how well the design scales as we add more AST node types and more operations on them, but it may be difficult to get a clear signal on that when we have so few of either of them (not to mention the fact that the same design might scale differently in C++ owing to the lack of pattern matching, ADTs, etc). For those purposes it might be more informative to look at existing C++ projects that have had to solve similar problems as a similar scale (Clang obviously leaps to mind here).

That said, two weeks is a small enough investment that I'm willing to take it on faith if you're confident that it will help us set a course for executable-semantics. I'm also happy to pitch in however I can, although that may not be much, because I have very little hands-on experience with Swift.

@austern:

I don't think the goal is to get actionable new information from Swift. I think the goal is just to serve the needs of the Executable Semantics project better: having an implementation of Carbon syntax that's so straightforward that it can serve as a specification as well as if it were English or BNF.

The claim is that it's not easy to do this if it's written in C++ but that it is easy to do this in a number of other languages, including Swift, Rust, and ML, and that in practice Dave can write it in Swift faster than in those other two languages.

@fowles:

I think the most important person to get on board here is @jsiek. From an overall direction point of view, at some point we may want a basic Swift style guide as well, but the core observation that C++ is not a great fit for this kinda thing is hard to disagree with.

@jsiek:

Catching up on this discussion now...

@geoffromer:

I don't think the goal is to get actionable new information from Swift. I think the goal is just to serve the needs of the Executable Semantics project better: having an implementation of Carbon syntax that's so straightforward that it can serve as a specification as well as if it were English or BNF.

My understanding is that @dabrahams is proposing a Swift implementation as a temporary means of gathering information to improve the C++ implementation (see e.g. "In order to make informed decisions about how to approach a C++ implementation..."), but it sounds like you're thinking of it as a way to permanently replace the C++ implementation.

I'm open to the possibility of a permanent language change, but I think it's a much harder sell. Among other things:

• It would mean that people need to be reasonably fluent in three different languages (C++, Carbon, and the new language) in order to meaningfully contribute to the design of Carbon.
• It could make it substantially harder to reach what I see as the long-term best option, which is for executable-semantics to be implemented in Carbon.

The claim is that it's not easy to do this if it's written in C++ but that it is easy to do this in a number of other languages, including Swift, Rust, and ML, and that in practice Dave can write it in Swift faster than in those other two languages.

If this is a two-week exploratory prototype, it makes a lot of sense to favor the language Dave will be most productive in, but if it's a permanent replacement for the C++ implementation, I think we need to focus much more on accessibility to future contributors. Among the languages that have the properties we want, Rust seems substantially more likely than Swift to be familiar to potential Carbon contributors, so if we're thinking of this as a permanent change, that's probably the language we should pick.

@dabrahams:

@austern has captured what I'm saying quite well, but there's a nuance that I should probably clarify.

If the only goal of executable semantics were, as Matt says, “having an implementation of Carbon syntax that's so straightforward that it can serve as a specification as well as if it were English or BNF,” then I wouldn't feel a need to rewrite it in C++. However, my understanding—based on having raised the possibility of using Rust a few weeks ago—is that the group also has the goal that executable semantics be implemented in C++. As long as that's the case, I am assuming that the Swift implementation will need to be translated.

The question @geoffromer asks about “actionable information” then becomes more relevant. My argument is that without a baseline view of what we “ought to” be able to achieve in terms of clarity, it will be very hard to judge which techniques work well in C++ and which C++ coding conventions are worth bending to achieve clarity.

HTH, Dave

@dabrahams:

It could make it substantially harder to reach what I see as the long-term best option, which is for executable-semantics to be implemented in Carbon.

Could you explain why that's best? It seems to me that we then have a "turtles" problem: the semantics of Carbon are defined in terms of Carbon.

@fowles:

I will offer a slightly heretical view here. I don't think executable semantics needs to make it back into C++. I think it could continue in Swift indefinitely and be fine. Additionally, if one of its major goals is easy of reading and modifying, I don't think that we are actually requiring deep knowledge of Swift here.

@jsiek:

I share Dave's concern regarding the amount of incidental complexity in the C++ implementation of the executable semantics.

I'd prefer to spend more time talking about Carbon and less time talking about low-level details of the implementation of the executable semantics. One benefit of switching to Swift, I hope, would be that some of those low-level details would go away, handled by Swift's support for safe unions.

That being said, I'm not exactly thrilled to reimplement what we've got so far and I'm worried about the "grass is always greener on the other side" effect.

On the whole, I think it makes sense to build a Swift version of the current executable semantics and then compare the two and see if indeed we get a more succinct implementation.

@geoffromer:

It could make it substantially harder to reach what I see as the long-term best option, which is for executable-semantics to be implemented in Carbon.

Could you explain why that's best? It seems to me that we then have a "turtles" problem: the semantics of Carbon are defined in terms of Carbon.

I see that as the best option because it will combine the advantages of the status quo (you only need to know C++ and Carbon to contribute) with the advantages of switching to Swift/Rust/etc (ADTs, pattern matching, hopefully coroutines, etc).

As for the "turtles", I don't see how this would be any more problematic than self-hosting a compiler. In fact, it's arguably somewhat less problematic: I assume that we will typically compile executable-semantics using the production Carbon toolchain, so there will be no circularity at the software level, and hence no room for "Reflections on Trusting Trust" -style shenanigans.

@dabrahams:

As for the "turtles", I don't see how this would be any more problematic than self-hosting a compiler.

Well, the self-hosting compiler implementation is usually not intended to act as a specification. I don't know about you, but I find definitions that depend on the thing being defined hard to understand unless there is a very clear base case and a very clear way to do a terminating induction with all other cases. For a factorial function, or quicksort, I understand how to do that. I don't think I know how to do that for a programming language.

@chandlerc:

Specifically commenting on the self-hosting and "turtles" problem:

If we get to the point where self-hosting is an option, I'm not really worried about turtles all the way down. The specification usage of executable semantics has to be pretty obvious from reading the code at a high level. It wouldn't really work for the specified behavior of Carbon to rely on the details of the implementation language used for executable semantics for any choice of implementation language: C++, Swift, Rust, Ocaml, or Carbon itself. The text of the code has to largely stand on its own for the purpose of specification. The fact that it is also executable helps ensure it doesn't have holes, and actually "works", but shouldn't be a significant part of the behavior itself.

Another way to look at it, the readers of executable semantics are unlikely to have a complete or perfect understanding of C++ or Swift, and will need to understand the specification of Carbon without gaining that deep understanding. So similarly, they should be able to understand the specification even if its turtles all the way down.

Anyways, I don't know that we need to sort that out right now. Backing up to the original point....

At a fundamental level, the tradeoff between continuing with Swift and translating back to C++ IMO is roughly: knowing the target, can we hide enough of the incidental complexity of C++ to make using C++ a smaller tax for the community than using Swift and C++ in the same project. If so, we should translate it to C++. If not, we should keep using Swift. While I suspect the answer will be "yes", I still think having the Swift example will be perfectly useful to make that decision and I'm interested in seeing it in case I'm wrong. =]

@dabrahams:

If we get to the point where self-hosting is an option, I'm not really worried about turtles all the way down. The specification usage of executable semantics has to be pretty obvious from reading the code at a high level. It wouldn't really work for the specified behavior of Carbon to rely on the details of the implementation language used for executable semantics for any choice of implementation language: C++, Swift, Rust, Ocaml, or Carbon itself. The text of the code has to largely stand on its own for the purpose of specification. The fact that it is also executable helps ensure it doesn't have holes, and actually "works", but shouldn't be a significant part of the behavior itself.

While something in me is still uncomfortable with Carbon's specification being written in terms of Carbon, I have to admit this all makes sense to me from a practical point-of-view.

Coming back to @geoffromer's earlier concern, I think I focused on the wrong aspect of it:

It could make it substantially harder to reach what I see as the long-term best option, which is for executable-semantics to be implemented in Carbon.

It seems to me that since the design of carbon is trying to accommodate expressive ADTs and structural pattern matching, translation from something like Swift into Carbon should be relatively straightforward, and at least wouldn't be hampered by incidental complexity as I expect translation from C++ would. There's nothing particularly esoteric about Swift and it has very few dark corners (unlike Rust, I'll note).

But all that said, I am not trying to make the case for a permanent change of language. If the group wants to make that decision after seeing the Swift code, it would be delightful, but it's not part of what I'm proposing.