Stream: wg-traits

Topic: bikeshedding "well formed"


nikomatsakis (Jan 22 2019 at 19:58, on Zulip):

In the weekly meeting discussion today, we talked about the current rules are using the phrase "well formed" in 3 distinct ways:

It seems like the latter two names should be altered, but not clear precisely to what.

centril (Jan 22 2019 at 20:03, on Zulip):

As I said before... this seems more confusing than helpful; now you have to explain the distinction between "legal" and "well-formed" when these two are actually more or less synonyms in natural language.

I think it would be better to state what sort of WF-ness it is; e.g. WFTrait(...), WFImpl(..) and whatnot...
This reduces "reasoning footprint" and ambiguity in the rules

centril (Jan 22 2019 at 20:04, on Zulip):

If you think "legal" is better... write LegalXyz(...) ;)

nikomatsakis (Jan 22 2019 at 20:05, on Zulip):

I don't see why we would have to explain this distinction

nikomatsakis (Jan 22 2019 at 20:05, on Zulip):

those two things are not comparable

nikomatsakis (Jan 22 2019 at 20:05, on Zulip):

that is, we don't have a notion of "well formed" that applies to (e.g.) an impl declaration

nikomatsakis (Jan 22 2019 at 20:05, on Zulip):

(if we choose to call it "legal", that is)

nikomatsakis (Jan 22 2019 at 20:06, on Zulip):

regarding this:

well-formed trait references T: Trait, which means that T: Trait is implemented and so are all of its where clauses

I like "fully implemented" for this, though it's maybe not perfect. But it gives me a much stronger intuition than "well-formed" ever did. =)

centril (Jan 22 2019 at 20:08, on Zulip):

@nikomatsakis all I'm saying is that "legal" and "wf" are synonyms; imo you gain nothing my having two words for it... just more confusion -- if you want to distinguish, talk about what sort of legality it is in the name

nikomatsakis (Jan 22 2019 at 20:11, on Zulip):

the reason I like "legal" is that it is a term people use ordinarily

nikomatsakis (Jan 22 2019 at 20:12, on Zulip):

i.e., if I were explaining Rust rules to some lay person, I would say "the impl is legal if blah blah blah is true"

nikomatsakis (Jan 22 2019 at 20:12, on Zulip):

I would never say to them "that impl is not well-formed"

centril (Jan 22 2019 at 20:13, on Zulip):

my point is not to debate which is more correct or better wrt. legal or WF...
using "legal" is fine, but then use it everywhere and drop WF entirely

centril (Jan 22 2019 at 20:13, on Zulip):

its just as fine to say "Vec<u8> is a legal type"

centril (Jan 22 2019 at 20:14, on Zulip):

e.g. LegalType(Vec<u8>) or LegalTraitRef(...)

nikomatsakis (Jan 22 2019 at 20:31, on Zulip):

Ah, I see. I think these are distinct concepts

nikomatsakis (Jan 22 2019 at 20:32, on Zulip):

that is, I don't know that I would use the term "legal" to describe the other two places we use "well-formed" presently

centril (Jan 22 2019 at 20:33, on Zulip):

@nikomatsakis so I haven't looked at the chalk docs in a while in the rustc guide... what are all the contexts WellFormed is for used currently?

nikomatsakis (Jan 22 2019 at 20:36, on Zulip):

Basically the first context is sort of "visible to end users" -- it describes the conditions that must be met or else a user error is reported. The other two contexts are more internal.

nikomatsakis (Jan 22 2019 at 21:27, on Zulip):

So, @centril, I believe that well-formed is used traditionally to basically mean "all names are in scope". I reviewed briefly the Wadler paper to double check that intuition, and it seems to match (let me know if you think I am mistaken). It's a very simple guarantee. For historical reasons (read: my fault), I somehow started using the term in a more expansive way in rustc.

The conditions I am describing via "legal" is sort of analogous to what the OK judgements in Featherweight Java (see Fig 7). I prefer legal to "OK" =)

nikomatsakis (Jan 22 2019 at 21:27, on Zulip):

(Incidentally, FJ also uses well-formed to mean "names are in scope")

nikomatsakis (Jan 22 2019 at 21:28, on Zulip):

well, wait

nikomatsakis (Jan 22 2019 at 21:28, on Zulip):

Screen-Shot-2019-01-22-at-4.28.18-PM.png

nikomatsakis (Jan 22 2019 at 21:29, on Zulip):

I take that back; in FJ, a "well-formed" type means something very similar to what we are using it to mean

centril (Jan 22 2019 at 21:29, on Zulip):

"ok" == WF :P

nikomatsakis (Jan 22 2019 at 21:29, on Zulip):

e.g., Foo<Bar> is only well-formed if Bar is a subtype of the bounds declared in the class

centril (Jan 22 2019 at 21:29, on Zulip):

e.g. "in Delta, T-bar is well-formed/ok"

nikomatsakis (Jan 22 2019 at 21:30, on Zulip):

I am presently leaning towards the following terms, in any case:

centril (Jan 22 2019 at 21:30, on Zulip):

what's the distinction btw fully and not?

nikomatsakis (Jan 22 2019 at 21:31, on Zulip):

Implemented means that we know there is an impl of the trait, but perhaps not for all the where clauses

nikomatsakis (Jan 22 2019 at 21:31, on Zulip):

so an impl provides a rule for Implemented but does not (in and of itself) prove DeeplyImplemented

centril (Jan 22 2019 at 21:31, on Zulip):

hmm... perhaps Satisfied(Foo: Bar) ?

nikomatsakis (Jan 22 2019 at 21:32, on Zulip):

I don't feel that captures the essential difference :)

nikomatsakis (Jan 22 2019 at 21:32, on Zulip):

nor is it a Rust term

nikomatsakis (Jan 22 2019 at 21:33, on Zulip):

put another way, "implemented" and "satisfied" feel sort of like synonyms to me

centril (Jan 22 2019 at 21:33, on Zulip):

hah =P

centril (Jan 22 2019 at 21:33, on Zulip):

fair

nikomatsakis (Jan 22 2019 at 21:35, on Zulip):

that said, it may not be worth bikeshedding too much on the name of the wf-trait-ref,

nikomatsakis (Jan 22 2019 at 21:35, on Zulip):

because I think it might make sense to do a deeper discussion of implied bounds

nikomatsakis (Jan 22 2019 at 21:35, on Zulip):

make sure the setup feels right

nikomatsakis (Jan 22 2019 at 21:35, on Zulip):

talk through what the things mean

nikomatsakis (Jan 22 2019 at 21:35, on Zulip):

and in the process maybe better names arise :)

nikomatsakis (Jan 22 2019 at 21:36, on Zulip):

I'm also pondering the alternative implied bounds formulation I described a bit back, I want to make sure I have a good gut feeling for what's wrong there

centril (Jan 22 2019 at 21:36, on Zulip):

yea I agree with agreeing about semantics before agreeing to labels; that might be what's missing

centril (Jan 22 2019 at 21:37, on Zulip):

e.g. it would be useful (for me) to see all the rules "in one place" and how they relate in a dense form

scalexm (Jan 23 2019 at 08:50, on Zulip):

@centril I (maybe naively) believe that this is what the chapter in the rustc-guide is for

nikomatsakis (Jan 23 2019 at 14:36, on Zulip):

there are two chapters in the rustc-guide:

Last update: Nov 12 2019 at 15:40UTC