Featherweight Swift (Formal Core Language)

[dabrahams (Dave Abrahams)]

@Alvae

@dabrahams

I'm not sure we're connecting.

It appears to be the case indeed, my apologies.

None needed; successful communication depends on all participants. It's as much my responsibility as yours.

@dabrahams

My point is that all of this low-level modeling of memory and pointers doesn't seem like it should be necessary in order to describe value semantics, and seems like it will result in a much more complicated model than necessary.

I argue that it depends on the purpose of the resulting formalization.

I agree!

Say I define some sort of operational semantics, i.e., the purely functional system you mentioned. Then yes, of course, I can model "mutation" in very simple terms. For instance, many lambda-calculi express assignment as simply as this:

let x := v in e ~> e[x/v]

Sorry, I'm afraid I don't know how to read that notation. Can you point me to a guide?

This is expressive enough, I assume, to describe the kind of formal definition you suggested. Nonetheless, notice that such a syntactic trick does not support "reference semantics". This, I believe, necessarily requires to model memory somehow.

Yes, memory (not necessarily raw memory, but something that allows two variables to be bound to the same mutable value) is required for reference semantics. But the useful properties of value semantics all stem from the fact that you can reason about the behavior of value semantic types without introducing the complexities associated with memory. It's similar to what happens when you create a purely functional programming language and run it on real hardware, which always has mutation: the formal description of the language becomes simpler, and reasoning about code becomes simpler. The difference is that with value semantics

• there's a more direct lowering to efficient machine code that takes advantage of the hardware's mutation, and
• the many computations that are most naturally expressed in terms of mutation can be expressed directly.

But this is still just math (to be fair, so are Alias Types).

Sorry, by “just math,” I meant that it doesn't require any programming-specific notions beyond those of traditional algebra, where a variable is actually just a name for one unchanging value. I didn't mean to suggest that Alias Types aren't mathematically well-founded; I'm sure that they are.

There also has been some interesting approaches to do this "syntactically"; see [1] and subsequent work from Elena Zucca.

I'll take a look.

Now the question is: what do I want from this?

Did you ever answer that question?

@dabrahams

I do think it's important to eventually be able to describe how types with value semantics can be built out of traditionally-unsafe parts like pointers and memory, but that doesn't seem necessary for the purposes of laying a foundation for value semantics.

If the goal is to formally illustrate the properties you described in your proposal, then I completely agree. We do not need the kind of models I suggested. In fact, if we look at your bullet points, the simple assignment semantics above can almost illustrate everything:

Whoa, how did you make those checkboxes? They don't show up in the quoted markdown.

Nit: you checked the first bullet, but I think to do that, you probably need to remove the word “independent,” which I take to effectively imply the 2nd-to-last bullet, which you didn't check (my list contains some intentional redundancy).

The two last points require a little more attention, because they are predicated upon a notion of reference.

Hmm, I'm not sure I buy that. They certainly don't use the word “reference” anywhere. They are predicated on the ability to alter the value associated with a variable. While that overlaps with the capabilities provided by what we think of as references, I claim it's significantly more restrictive.

This comes back to what I meant about the requirement to model memory as some sort of "store", so that two names can refer to the same thing.

Sorry, you lost me. I don't understand how you conclude there's a need to discuss names “referring” to anything from the language in those two bullets.

I like @Lantua's definition of so-called points of access (see Avoiding unbreakable reference cycle with value types and closures?) to describe this concept.

That seems like a useful way to describe a world with both value and reference semantics.

We can model such a store in the "conventional" way, by the means of an ad-hoc data structure, or in the style of [1]. In the former case, I guess it would look something like the following:

S; var x := v in e ~> S, x=v; e[x/ref(x)]
S, x=v1; ref(x) := v2 in e ~> S, x=v2; e

Again, I'll need some help with that notation.

We obtain a very simple framework (I don't even need types!) to formally illustrate your bullet points. We may also prove them on terminating programs.

...

I hope this makes sense, and that I didn't mischaracterise your point.

That all sounds very interesting, but I'm afraid it doesn't make sense to me yet; I look forward to the moment where my understanding catches up with what you wrote

By the way, I'm open to move this discussion to a phone call, even if it means summarizing the exchange in text here afterwards.

Thanks for the offer. For the time being, I'd like to keep it here, though. The written form gives me enough time to consider everything you say, follow references, etc. without worrying about being frustratingly slow.