Stream: t-compiler/wg-polonius

Topic: meeting 2019.09.10


lqd (Sep 10 2019 at 19:03, on Zulip):

do we have a meeting tonight ? :)

lqd (Sep 10 2019 at 19:04, on Zulip):

if so, I have a small-ish update: I have been working on the polonius inputs doc here

lqd (Sep 10 2019 at 19:07, on Zulip):

it's not much yet, but it did make me wonder if 1) I should try to (understand, then) talk about the liveness inputs ? 2) how deep should these pre-liveness inputs be described ? (especially wrt fact generation in rustc itself, and that any very precise description will have to be kept in sync, while things are not yet finalized on all analyses)

lqd (Sep 10 2019 at 19:08, on Zulip):

(I wasn't able to find the time yet but I'm excited to read Albin's thesis soon)

nikomatsakis (Sep 10 2019 at 19:09, on Zulip):

:wave:

nikomatsakis (Sep 10 2019 at 19:10, on Zulip):

that's a good question

nikomatsakis (Sep 10 2019 at 19:10, on Zulip):

I think a relatively light coverage would suffice, but I do think it'd be good to be striving for a canonical reference that is not the code

lqd (Sep 10 2019 at 19:11, on Zulip):

can it be worked on a bit at a time ? or should it be relatively complete before merging ?

nikomatsakis (Sep 10 2019 at 19:11, on Zulip):

I think it can be grown over time for sure

nikomatsakis (Sep 10 2019 at 19:12, on Zulip):

I was just debating whether it makes more sense to collab in a hackmd

nikomatsakis (Sep 10 2019 at 19:12, on Zulip):

but prob better to merge and maybe do some successive PRs?

nikomatsakis (Sep 10 2019 at 19:12, on Zulip):

anyway my main thing is that I plan to book some time this week to get to polonius

lqd (Sep 10 2019 at 19:12, on Zulip):

I'm not super satisfied with the current hackmd yet so I didn't open a PR

nikomatsakis (Sep 10 2019 at 19:12, on Zulip):

because it didn't happen last week

nikomatsakis (Sep 10 2019 at 19:12, on Zulip):

part of that would be reviewing @Albin Stjerna's draft

lqd (Sep 10 2019 at 19:13, on Zulip):

awesome

lqd (Sep 10 2019 at 19:13, on Zulip):

there are a couple points in last week's list, and meta-planning in general, which could be interesting, whenever you get the chance

Albin Stjerna (Sep 10 2019 at 19:14, on Zulip):

Oh right hey sorry I forgot about the meeting

Albin Stjerna (Sep 10 2019 at 19:15, on Zulip):

Fortunately I was summoned :)

Albin Stjerna (Sep 10 2019 at 19:16, on Zulip):

I would be happy to document the liveness stuff

lqd (Sep 10 2019 at 19:16, on Zulip):

(if you want to collab on a hackmd niko, we can use the earlier link to the WIP)

Albin Stjerna (Sep 10 2019 at 19:17, on Zulip):

Sure!

nikomatsakis (Sep 10 2019 at 19:17, on Zulip):

(if you want to collab on a hackmd niko, we can use the earlier link to the WIP)

yeah maybe that's a good start

nikomatsakis (Sep 10 2019 at 19:17, on Zulip):

I guess .. hmm .. if I had an hour for polonius

nikomatsakis (Sep 10 2019 at 19:17, on Zulip):

maybe the best use of it is not to try and write some docs

nikomatsakis (Sep 10 2019 at 19:17, on Zulip):

but rather to explore some of the "open-y questions??

Albin Stjerna (Sep 10 2019 at 19:17, on Zulip):

Probably not

nikomatsakis (Sep 10 2019 at 19:17, on Zulip):

e.g., providing feedback to @lqd on the "equality relation" variant of the rules,

nikomatsakis (Sep 10 2019 at 19:17, on Zulip):

or the subset-eq etc?

Albin Stjerna (Sep 10 2019 at 19:18, on Zulip):

Also, can I review PRs?

Albin Stjerna (Sep 10 2019 at 19:18, on Zulip):

We got some nice small fixes from @Tshepang Lekhonkhobe and I think merging them would be a no-brainer

lqd (Sep 10 2019 at 19:20, on Zulip):

@nikomatsakis maybe yeah, I'll do the doc myself, so you can focus on more important things. there was also the illegal subset errors vs optimization question, and the OOM question where we materialize too much stuff today (maybe the equality relation would help, if it was done in rustc; but still unclear to me as of yet)

lqd (Sep 10 2019 at 19:21, on Zulip):

@Albin Stjerna you can for sure "review" on github, I don't think we have bors anymore, so maybe not merge per se, but I can do that just ping me :)

nikomatsakis (Sep 10 2019 at 19:21, on Zulip):

Also, can I review PRs?

let me make that happen...

lqd (Sep 10 2019 at 19:21, on Zulip):

even better

Albin Stjerna (Sep 10 2019 at 19:22, on Zulip):

I figure it's good to waste as little of your mental bandwidth as possible

Albin Stjerna (Sep 10 2019 at 19:23, on Zulip):

@lqd But should I add the liveness stuff to your HackMD?

lqd (Sep 10 2019 at 19:23, on Zulip):

sure why not :)

Albin Stjerna (Sep 10 2019 at 19:23, on Zulip):

I think I will wait until I have ironed out the kinks of the initialisation post-thesis, but liveness shouldn't change at all

nikomatsakis (Sep 10 2019 at 19:23, on Zulip):

to clarify my motivations re: book

nikomatsakis (Sep 10 2019 at 19:23, on Zulip):

I found it kind of hard to review the initialization stuff

nikomatsakis (Sep 10 2019 at 19:24, on Zulip):

that is, I'd sort of rather try to review such things in conjunction with a nice write-up

lqd (Sep 10 2019 at 19:24, on Zulip):

ah interesting

nikomatsakis (Sep 10 2019 at 19:24, on Zulip):

that tries to "extract" the relations

nikomatsakis (Sep 10 2019 at 19:24, on Zulip):

anyway, I tink it's good to be working on it together,

Albin Stjerna (Sep 10 2019 at 19:24, on Zulip):

I think that makes total sense, and it would also make onboarding much, much easier

nikomatsakis (Sep 10 2019 at 19:24, on Zulip):

I will I think try to focus a bit on the equality stuff

nikomatsakis (Sep 10 2019 at 19:25, on Zulip):

I never really explored what @lqd did and it seems important to settle that a bit

nikomatsakis (Sep 10 2019 at 19:25, on Zulip):

in particular I think (trying to remember why now :) it impacts a bit how we formulate the region error work

nikomatsakis (Sep 10 2019 at 19:25, on Zulip):

well, the main thing there is

nikomatsakis (Sep 10 2019 at 19:25, on Zulip):

my original formulation was done by looking for illegal subset relations

nikomatsakis (Sep 10 2019 at 19:26, on Zulip):

and I thk I decided that I don't want to do that, I want to use 'placeholder loans' to represent things like 'a and friends

Albin Stjerna (Sep 10 2019 at 19:26, on Zulip):

I also think we will need a decision soon-ish on how other types of errors are to be reported

lqd (Sep 10 2019 at 19:26, on Zulip):

(the reason I mention the illegal subset errors vs optimization is that we can make the naive version as fast as location insensitive today, if we don't do the subset TC)

Albin Stjerna (Sep 10 2019 at 19:26, on Zulip):

For example move errors

nikomatsakis (Sep 10 2019 at 19:26, on Zulip):

precisely because the subset relations should be considered the "type inference" part of things, i.e., you should be able to create a type system where each origin O is replaced with a set of loans {L} and you don't have to track the subset relations between origins

nikomatsakis (Sep 10 2019 at 19:26, on Zulip):

er, provenances?

nikomatsakis (Sep 10 2019 at 19:26, on Zulip):

"origins" feels kind of good :)

nikomatsakis (Sep 10 2019 at 19:26, on Zulip):

which reminds me that we need to settle on terminology

nikomatsakis (Sep 10 2019 at 19:27, on Zulip):

all I can say for sure is that regions is ungreat

Albin Stjerna (Sep 10 2019 at 19:27, on Zulip):

Yes, which I presume a book is also good for?

nikomatsakis (Sep 10 2019 at 19:27, on Zulip):

right

nikomatsakis (Sep 10 2019 at 19:27, on Zulip):

I think maybe that is a good start -- let's just try to write down the "table of contents"

lqd (Sep 10 2019 at 19:27, on Zulip):

I find all the terminology has a connotation of "places" which are not really "sets of loans" ?

nikomatsakis (Sep 10 2019 at 19:27, on Zulip):

and we can haggle over the names

nikomatsakis (Sep 10 2019 at 19:27, on Zulip):

a loan is the combination of a place and a mutability, basically

nikomatsakis (Sep 10 2019 at 19:28, on Zulip):

"a place that was borrowed, and how it was borrowed"

nikomatsakis (Sep 10 2019 at 19:28, on Zulip):

(that said, I secretly wish that we had used the term shared for &T and borrowed for &mut T -- since borrowing seems to imply "original owner no longer has it")

nikomatsakis (Sep 10 2019 at 19:28, on Zulip):

(but in that case I'm not sure what the term would be that encompasses both)

nikomatsakis (Sep 10 2019 at 19:28, on Zulip):

a loan is the combination of a place and a mutability, basically

feel free to tell me it's an ungreat bit of terminology, too

lqd (Sep 10 2019 at 19:29, on Zulip):

yeah makes sense, I'll adapt :)

nikomatsakis (Sep 10 2019 at 19:29, on Zulip):

I find all the terminology has a connotation of "places" which are not really "sets of loans" ?

oh, I See what you're saying here

Albin Stjerna (Sep 10 2019 at 19:29, on Zulip):

I'll pretend I never heard any of this until my thesis has landed

nikomatsakis (Sep 10 2019 at 19:29, on Zulip):

well, I think the answer is:

nikomatsakis (Sep 10 2019 at 19:29, on Zulip):

a references is created by a loan

nikomatsakis (Sep 10 2019 at 19:29, on Zulip):

and the origin of the reference

nikomatsakis (Sep 10 2019 at 19:29, on Zulip):

is that set of loans it may have come from

nikomatsakis (Sep 10 2019 at 19:29, on Zulip):

does that sound coherent?

lqd (Sep 10 2019 at 19:30, on Zulip):

sure

Albin Stjerna (Sep 10 2019 at 19:30, on Zulip):

yes

lqd (Sep 10 2019 at 19:30, on Zulip):

origin is tempting as well :)

lqd (Sep 10 2019 at 19:31, on Zulip):

and also has the advantage of not starting with P which we use for CFG points and their type

nikomatsakis (Sep 10 2019 at 19:31, on Zulip):

ha yes

nikomatsakis (Sep 10 2019 at 19:31, on Zulip):

I was wondering about that

nikomatsakis (Sep 10 2019 at 19:31, on Zulip):

I guess you could use .. N for proveNance?

nikomatsakis (Sep 10 2019 at 19:31, on Zulip):

V is clearly variable

nikomatsakis (Sep 10 2019 at 19:32, on Zulip):

so actually do we have a table of the "atoms" and their letters? :)

lqd (Sep 10 2019 at 19:32, on Zulip):

:)

nikomatsakis (Sep 10 2019 at 19:32, on Zulip):

we could also -- bear with me here --

nikomatsakis (Sep 10 2019 at 19:32, on Zulip):

write out actual words :P

nikomatsakis (Sep 10 2019 at 19:32, on Zulip):

/me slowly learning that academic style is not actually very self documenting

lqd (Sep 10 2019 at 19:33, on Zulip):

and the datalog rules can stay as is even if we use more descriptive words elsewhere

Albin Stjerna (Sep 10 2019 at 19:33, on Zulip):

A really quick way to learn that is to teach Haskell as a first programming language at an introductory computer programming course

Albin Stjerna (Sep 10 2019 at 19:34, on Zulip):

I started to use longer names in those too, which may or may not be a good idea

lqd (Sep 10 2019 at 19:35, on Zulip):

as we're running out of time, this week I'll continue on the doc and try to read Albin's thesis

Albin Stjerna (Sep 10 2019 at 19:36, on Zulip):

Note that my thesis should contain a complete list of all inputs with descriptions and the relations

lqd (Sep 10 2019 at 19:36, on Zulip):

IIUC Albin will use their newfound reviewing-merging powers to merge the couple PRs in flight (and maybe write a bit about liveness facts in the hackmd)

Albin Stjerna (Sep 10 2019 at 19:36, on Zulip):

And a table with Official Shorthands

Albin Stjerna (Sep 10 2019 at 19:36, on Zulip):

All of which may be suboptimal and/or wrong :)

Albin Stjerna (Sep 10 2019 at 19:37, on Zulip):

But thanks, I do appreciate the effort

lqd (Sep 10 2019 at 19:38, on Zulip):

and if time permits Niko will do Niko-ish things such as looking at the "equality stuff" (we need a name for that as well :)

Albin Stjerna (Sep 10 2019 at 19:38, on Zulip):

pasted image

lqd (Sep 10 2019 at 19:38, on Zulip):

sounds good ?

Albin Stjerna (Sep 10 2019 at 19:39, on Zulip):

That's what I used for a placeholder

lqd (Sep 10 2019 at 19:39, on Zulip):

nice as well

lqd (Sep 10 2019 at 19:40, on Zulip):

and of course, thank you for your time everyone :) :wave:

Tshepang Lekhonkhobe (Sep 10 2019 at 19:42, on Zulip):

write out actual words :P

this gets my vote... was looking at the code yesterday, had to write it down to make sense of it, and wondered why we aren't spelling out them words

Last update: Nov 15 2019 at 21:05UTC