A Stateful MIR for Rust

language design
1

A too-long note on the presentation: I proposed that a number of features I want are interrelated, and in https://github.com/rust-lang/rfcs/pull/1617#issuecomment-220717843 @nikomatsakis suggested I open an internals thread if I wanted to discuss such things. Yet here I am writing in a GitHub repo. Why? A tension between three goals.

First I want to present these ideas together in one single post, as my main technical point is the way the concepts relate rather than the concepts themselves. If the features are sufficiently related, trying to tackle them all at once may be more productive, rather than a futile overextension of limited language design resources.

Second, this nevertheless proved to be such a huge post that I decided it would be better to release it in installments. The errors I’ll inevitably make would be best caught as soon as possible lest they derail my reasoning in the sections that follow them. And there’s always the risk I would get stuck and not finish. Finally, errors aside, whatever discussion the earlier sections generate will no doubt help in writing the later sections.

Third, it is unclear to me if Discourse publicly exposes posts’ edit history, and for anybody reading the thread it would be absolutely necessary to view the state of this proposal at the time a post was written.

So, I hope that with the github repo anybody can both read the proposal in its latest form, with all criticism and suggestions (hopefully!) taken into account, and also follow the thread, going through the git history as necessary. I’ll do my best to comment when I push a new commit.

This first installment lays out the kernel of what I propose, along with a (sized-indexed) uninitialized type. It may be a bit under-motivated on its own, but I hope what’s to come will fix that.

1 Like
2

Can you try to be more in-line with the structure of the current MIR, except in places that need to be changed?

BTW, what’s a sized-indexed type?

3

I think this is definitely very important. The document you've presented discusses adding a huge amount of complexity to the language in a manner which is abstracted far away from user stories and use cases. Without a clear idea of the motivation, its hard to imagine adding all of these language features to Rust.

2 Likes
4

Can you try to be more in-line with the structure of the current MIR, except in places that need to be changed?

Do you have an example of a difference that looks unnecessary? I tried to look at the librustc type definitions and emulate them, but 1) for formalization purposes I wanted to not rely on inference, multiple passes, side tables, etc, and 2) for both my and readers' sanity, I wanted to not tackle reformulating all of the MIR at once. And as I write more sections I'll incrementally add things back and modify the definitions I've written so far. After I'm done, I'll make an appendix with all the rules in their final form, and I'd happy to also think about the minimal changes needed for rustc to implement this specification. Does that sound good?

BTW, what's a sized-indexed type?

Oh, an "indexed type" usually means a type that takes a value parameter. By "sized-indexed" I meant there'd be not one uninitialized type, but one for each size, analogous to [u8; n].

5

One big thing to keep in mind is that since I am specifying a core language, nothing here is a forwards compatibility or teaching hazard. As to the motivation, well wait and see :). If I succeed, this will be the first presentation to safely account for all the features I list at the top.

6

I think "size-indexed" would be more standard. "sized-indexed" sounds like "type-indexed, except the types must be sized".

Plus [u8; n] is not size-indexed. It is length-indexed.

7

Oh haha, sizedd was a typo on my part the whole time. Thanks for catching that.

[u8; n] is length-indexed

True; I chose u8 to best approximate since, as far as I know, our sizes have 1 byte granularity.

8

First, MIR does not have side-tables.

I was mostly surprised by the arg/local/retslot distinction. The distinction you are interested in is their state in function start/end, right?

Any interesting model here should handle panics - they have the interesting effect of allowing functions to either initialize a place or not, depending on which edge you branch through. I understand not doing it for an MVP tho.

Also, rustc lvalues refer to both base lvalues and projections. Projections are rather interesting (at least fields - I don't think you have to handle subslices from the start).

If you want to simplify, I would suggest removing rvalues except for use and ref - they can't do anything function calls can't do, except for being nounwind.

9

I assume your basic block embedding is the standard CPS-within-a-Y-combinator?

BTW, I would like you to be more specific on types. Rust types have 1 kind (+ maybe another kind for constants), and they can be passed to type constructors, be projected from associated types, etc.

If you are introducing more kinds, you should be more clear about that.

10

I was mostly surprised by the arg/local/retslot distinction. The distinction you are interested in is their state in function start/end, right?

Yes. There is only one kind of lvalue as far as anything in the function body is concerned. I only distinguished them in the grammar for the sake of the Fn rule for the types of the start end nodes---the "state in function start/end" exactly as you say.

Any interesting model here should handle panics - they have the interesting effect of allowing functions to either initialize a place or not, depending on which edge you branch through. I understand not doing it for an MVP tho.

IIUC panics edges are barely distinguished from normal control flow, but static drop flags are quite interesting. For the former, I'll at some point comment one can give Fn and additional predefined unwind node, and for the latter I basically dedicate the "Dynamism" section I hint at in the intro.

Also, rustc lvalues refer to both base lvalues and projections. Projections are rather interesting (at least fields - I don't think you have to handle subslices from the start).

Yes projections are very interesting. Next on the docket are a lifetimes and unique references section, where I'll introduce deref projection. Partial Moves in my system seem to necessitate that types of fields can change independently of their owner---that's weird and will get a lot of attention. [N.B. I think you were there on IRC when I proposed making deref not a projection as only the ref value, not the location of the ref is stored in, is needed. I think I'll hold off on that for the time being as its a somewhat orthogonal problem, and a hard one too.]

If you want to simplify, I would suggest removing rvalues except for use and ref - they can't do anything function calls can't do, except for being nounwind.

Heh I forgot to introduce call so far! I guess I should do that soon as references used within functions and references sent between functions have so-far struct me as wanting surprisingly different properties. I introduced those other rvalues precisely because they don't seem to interact with much, so it was complexity I could afford to not delay including :). Hopefully that doesn't just impose extra noise value on the reader at this stage.

11

The entire point of &move is that it allows you to treat dereferences of it as a projection lvalue.

The interesting detail is that the returned typestate depends on which edge you take. I don't think this is very complicated to handle, but it may be interesting.

12

I'm not familiar with that, are you saying the basic blocks themselves need to be built with a Y-combinator, or the blocks are tied together into a function with a Y-combinator? If the latter, I might have rediscovered this :). Fn is like letrec-in, without the in. To keep things simple, there are no basic blocks. Each bound label points to one node, not one basic block / chain of nodes, and successors are always "top-level" bound labels rather than nodes inline.

I realize now my Fn adds both entry and exit into the context, when entry must be defined explicitly. I'll fix that. edit now fixed.

13

The entire point of &move is that it allows you to treat dereferences of it as a projection lvalue.

You responding to the [N.B. ...]? I agree that deref must yield an lvalue for precisely that reason. I'm not convinced that the ref being dereferened need be an lvalue too, but haven't formalized a good alternative yet.

The interesting detail is that the returned typestate depends on which edge you take. I don't think this is very complicated to handle, but it may be interesting.

I already do support different branches initializing variables different ways, though the typestate must match on a merge. From a panicking perspective, that's the "eager static drop" RFC. I just need to add some dynamism corresponding to stack flags---the typestate will still match on merge, but match by "forgetting" whether something is initialized or not.

14

First, it's not the "eager static drop" RFC, because it does not insert the drops (being a MIR-level semantics, that is not its job).

If you can figure out a nice way to connect dynamic stack flags, that would be nice.

15

First, it's not the "eager static drop" RFC, because it does not insert the drops (being a MIR-level semantics, that is not its job).

Yeah definitely. One could interpret that RFC as adding restrictions to the surface language such that it could be desugared to the IR I've defined so far.

If you can figure out a nice way to connect dynamic stack flags, that would be nice.

The basic idea (which is all I've worked out so far) would have enums for with initialized and uninitialized variants. Enum subtypes like in my "enum switch" section would remove the need for dynamic checks outside of unwinding. The annoying complication is that partial moves necessitate putting the enum tag somewhere else.

16

OK, whew! Some changes:

  • Completed draft of non-lexical lifetimes and “outlives-at” formulation. I’ll proofread it tomorrow, but besides any typos I think I have a pretty exhaustive treatment here :slight_smile:.
  • Based on what @arielb1 pointed out, I added a Call node, and changed “sized-index” to “size-index”. Thanks again!
  • There actually isn’t any continuation width subtyping based on the lvalue context—all lvalues must be given types all the time.
  • Misc things I already forget, see the commit message.
1 Like
17

Generalized unique references section draft has been up. Biggest difference is contravariance is now optional, since we don’t currently have it.

CC @aturon as requested

18

This is epic! I suspect it’s already longer than nearly(?) every RFC in the repo.

1 Like
19

People with this level of type-fu are precious.

1 Like
20

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.