WG-Traits Minutes and General Discussion

[nikomatsakis]

Update from 2018.04.02 meeting

Updates. There are a number of exciting updates from last week in the dropbox paper. If you’re enjoying following along on everyone’s progress, definitely check it out!

Goals for this week. This week, the focus will be on pushing towards connecting rustc and the SLG solver. Here are the highlights of work to be done:

• We should finish off the chalk lowering rules:
  • Rule WellFormed-TraitRef
  • Rule ProjectionEq-Normalize
  • Rule ProjectionEq-Skolemize
• Urgent: We need a query to figure out the program clauses that can solve a given domain goal (#49600). I’ve started this and can keep hacking on it, but if someone is keen and has some spare time over this week, I’d love to collaborate, as I’m pretty hard up for time right now.
• The GAT rules that @scalexm was hacking on need to be written out in rustc-guide and implemented in rustc.

Things that need documenting. The traits-guide coverage of higher-ranked bounds and universes is not really done. There is some coverage under region solving, but it needs to be moved into the trait section. I’d be happy to work with someone who wants to learn that stuff and hence keep extending the trait docs.

[nikomatsakis]

And a poll! There is a question I forgot to raise! We sometimes use the term “skolemized” in Chalk and rustc to refer to “free, universally quantified names”. So for example if we solving a higher-ranked trait bound like for<'a> { T: Foo<'a> }, we would substitute a “skolemized region” in for 'a, yielding T: Foo<'!0>. These !-types and regions (not to be confused with the never type…) are kind of a representative that stands in for “some unknown lifetime”; it works exactly like talking about T in the body of a generic function fn foo<T> { ... }.

Anyway, the name skolemized is not good for two reasons:

• It is confusing to newcomers and very obscure.
• We’re probably using it wrong anyway. From what I can tell, skolemization is generally defined as removing existential quantifiers and replacing them with universal ones, but here we are…not doing that.
  • This is weird. I took the name from the epic “Practical Type Inference for Arbitrary Rank Types” paper, but I can’t tell if they are also using it in an unusual way, or if it is correct in that case for some reason.

So, what I am leading up to here is: what name should we adopt instead? I have been torn between “forall type/region” and “universal type/region”. I want something that is at least somewhat intuitive. I think another term sometimes used is eigenvariable, but that does not seem more obvious. I’m leaning towards ‘forall variable’, on the basis that “universally quantified” is more jargon-y than “forall”, but…

[sgrif]

forall type/region gets my vote. It most closely ties it to the actual syntax it represents in Rust. eigenvariable has a weird conflict w/ eigenclass in Ruby for me.

[mark-i-m]

So, what I am leading up to here is: what name should we adopt instead?

Matsakified

In seriousness, I think I would prefer something that lends itself nicely to being abbreviated. Also, the name should make it clear that the region is not universally qualified, which is perhaps a bit counterintuitive from a name like “forall variable”… maybe something like “dequalified variable” or “de-foralled”?

[tmandry]

Would “wildcard type” or “wildcard region” work? It ties into (I think) a familiar term for most programmers. Perhaps it doesn’t carry enough of the underlying meaning, though.

[Tom-Phinney]

IIRC, it is an abstraction of a specific item, so perhaps just prefixing the item noun (or other term) with the qualifier „abstract" would suffice.

[mark-i-m]

I feel like that is too abstract

[mark-i-m]

How about “FUIFA variables”: For Unknown Implies ForAll

[sgrif]

Why is it important to make it something that is easily abbreviated?

[mark-i-m]

Less writing. It also allows us to have a more descriptive name without worrying as much.

Moreover, what great design is complete without an acronym or abbreviation

[Centril]

My preference is for terms which you can easily search for with google so that you can find definitions and related literature. If “skolemized” accurately describes the intent or is close enough, then that should be kept, if not, it shouldn’t be and we should pick something more accurate in the PLT literature.

[djc]

You know that Elon Musk in his companies has forbidden the use of acronyms, right? They make your language actively harder to penetrate for anyone new coming up to speed on your jargon.

[yarrow]

It looks like mathematicians use “Skolemization” for the process of removing existential quantifiers by a process that introduces constant and function symbols, and Herbrandization for the dual process of removing universal quantifiers. But folks working in automated theorem proving seem to use skolemization in the broadened sense of removing quantifiers, both universal and existential.

So the usage is correct in this context. On the other hand, a google search for “skolemized” is much more likely to bring up the mathematical sense of Skolemization than the theorem-proving sense.

The only thing that comes to my mind as a replacement for “skolemized” is “de-quantified” type or region, but I think that’s even more confusing.

[gbutler]

You know that Elon Musk in his companies has forbidden the use of acronyms, right?

Good thing we have Elon to tell us the right way to do things. I’m sure that all the organizations that regularly use acronyms CORRECTLY (important point) can’t wait to get rid of them.

Correct use of acronyms are to use the full, expanded version at the first use in a communication followed by the acronym in parenthesis. Then, in the remainder of the communication, just use the acronym. If the communication is long (like a book with several chapters), you should use the full, expanded version at the first use in each chapter. A couple of page essay, memo, tutorial, or press-release would be correct to only use the full, expanded version at the first use in the document.

If those rules are followed, acronyms ABSOLUTELY facilitate clear, concise communication.

[nikomatsakis]

I think I like the following terms best:

• “bound variable”
  • the (second) X in forall<X> { X: Foo }
    • that is, a reference back to a binder that has not been “removed” from the term
• “forall variable”
  • when we remove the forall<X> binder, we get !0: Foo – that !0 is a “forall variable”
• “exists variable”
  • an inference variable, which arises from removing a exists<X> { ... } binder in a goal (or instantiating a forall<X> binder in a clause)

[rpjohnst]

@gbutler- could you please use a little less snark and all-caps here (and in general)? It’s enough to make your point well once and let others make theirs.

[mark-i-m]

“forall variable”

when we remove the forall<X> binder, we get !0: Foo – that !0 is a “forall variable”

I still find this a bit counterintuitive. A forall variable is one where we removed (skolemized) the forall…

[nikomatsakis]

I still find this a bit counterintuitive. A forall variable is one where we removed (skolemized) the forall…

Perhaps; I think the implicit thing is that it is a “free” forall variable - i.e., the binder has moved “out” of the term, and this is telling you what sort of binder it was.

[mark-i-m]

I guess that’s fair. I don’t have really strong feelings… I just feel like the name should communicate a bit more about why we are skolemizing: if we can prove that something is true for an arbitrary unknown X, then we can prove it forall<X>… When I was reading your PR in the rustc-guide about skolemization, the paragraph where you explained that is where everything clicked for me

[nikomatsakis]

One good thing about the term “skolemize” is that it is quite unique, making it easy to look up the definition. “forall” doesn’t seem to share this property. Perhaps there is another term that can capture this intuition and be sort of unique. “Universal stand-in”? “Representative”? “Exemplar”? “Specimen”? (Can you tell I’m looking at a thesaurus…? )