Clean up skolemization with placeholder #217

csmoe · 2018-10-24T06:48:19Z

mark-i-m

Thanks! Overall, looks good :)

One thing is that "placeholder" seems a bit weird when used as a verb. I would propose "placeholder-ify", "placeholdered", and "placeholdering". I left comments where I think we might want to change.

Also, I left a couple of nits/typos/minor comments.

src/appendix/glossary.md

mark-i-m · 2018-10-24T16:13:17Z

src/traits/hrtb.md

@@ -36,20 +36,20 @@ to the subtyping for higher-ranked types (which is described [here][hrsubtype]
 and also in a [paper by SPJ]. If you wish to understand higher-ranked
 subtyping, we recommend you read the paper). There are a few parts:

-**TODO**: We should define _skolemize_.
+**TODO**: We should define _placeholder_.


I think we can remove this TODO and just link to the glossary?

mark-i-m · 2018-10-24T16:14:22Z

src/traits/hrtb.md

@@ -78,7 +78,7 @@ impl Foo<&'static isize> for StaticInt;

 We want the obligation `StaticInt : for<'a> Foo<&'a isize>` to be
 considered unsatisfied. The check begins just as before. `'a` is
-skolemized to `'0` and the impl trait reference is instantiated to
+placeholder to `'0` and the impl trait reference is instantiated to


mark-i-m · 2018-10-24T16:15:45Z

src/borrow_check/region_inference.md

  corresponds (intuitively) to some unknown set of other elements –
-  for details on skolemization, see the section
-  [skolemization and universes](#skol).
+  for details on placeholder, see the section


Suggested change

for details on placeholder, see the section

for details on placeholders, see the section

mark-i-m · 2018-10-24T16:15:54Z

src/borrow_check/region_inference.md

-  for details on skolemization, see the section
-  [skolemization and universes](#skol).
+  for details on placeholder, see the section
+  [placeholder and universes](#placeholder).


Suggested change

[placeholder and universes](#placeholder).

[placeholders and universes](#placeholder).

mark-i-m · 2018-10-24T16:18:03Z

src/borrow_check/region_inference.md

@@ -198,7 +198,7 @@ fn bar<'a, T>(t: &'a T) {
 ```

 Here, the name `'b` is not part of the root universe. Instead, when we
-"enter" into this `for<'b>` (e.g., by skolemizing it), we will create
+"enter" into this `for<'b>` (e.g., by placeholder it), we will create


mark-i-m · 2018-10-24T16:19:09Z

src/borrow_check/region_inference.md

@@ -411,7 +411,7 @@ for<'a> fn(&'a u32, &'a u32)
 for<'b, 'c> fn(&'b u32, &'c u32)
 ```

-Here we would skolemize the supertype, as before, yielding:
+Here we would placeholer the supertype, as before, yielding:


Typo:

Suggested change

Here we would placeholer the supertype, as before, yielding:

Here we would placeholder the supertype, as before, yielding:

mark-i-m · 2018-10-24T16:19:55Z

src/borrow_check/region_inference.md

@@ -476,7 +476,7 @@ an error. That's good: the problem is that we've gone from a fn that promises
 to return one of its two arguments, to a fn that is promising to return the
 first one. That is unsound. Let's see how it plays out.

-First, we skolemize the supertype:
+First, we placeholder the supertype:


src/traits/caching.md

mark-i-m · 2018-10-24T16:20:43Z

src/traits/hrtb.md


 [hrsubtype]: https://github.com/rust-lang/rust/tree/master/src/librustc/infer/higher_ranked/README.md
 [paper by SPJ]: http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/

 So let's work through our example.

 1. The first thing we would do is to
-skolemize the obligation, yielding `AnyInt : Foo<&'0 isize>` (here `'0`
-represents skolemized region #0). Note that we now have no quantifiers;
+placeholder the obligation, yielding `AnyInt : Foo<&'0 isize>` (here `'0`


csmoe · 2018-10-25T03:00:27Z

@mark-i-m while re-review niko's PR, when talking about "placeholder-ify", the diff wrote "replace .. with placeholder" or "create/add placeholder". so I decide to follow his words, is this ok?

mark-i-m

Excellent! Thanks @csmoe.

LGTM. I left a few nits/minor changes. I tried to use Github's new suggestions feature. Let me know how it works. After that, r=me 😄

src/borrow_check/region_inference.md

src/traits/hrtb.md

src/traits/caching.md

Co-Authored-By: csmoe <[email protected]>

csmoe · 2018-10-25T03:34:27Z

r? @mark-i-m it works 😄

mark-i-m · 2018-10-25T04:22:47Z

Thanks @csmoe 😄

clean up skolemiza in glossary

f70db41

mark-i-m suggested changes Oct 24, 2018

View reviewed changes

csmoe added 2 commits October 25, 2018 10:33

clean up skolemiza in borrow_ck

5a11c34

clean up skolemiza in traits

c7c309d

csmoe force-pushed the placeholder branch 4 times, most recently from 2e1b236 to 659386f Compare October 25, 2018 03:15

replace bound region with placeholder

9a69b6f

csmoe force-pushed the placeholder branch from 659386f to 9a69b6f Compare October 25, 2018 03:20

mark-i-m reviewed Oct 25, 2018

View reviewed changes

src/borrow_check/region_inference.md Outdated Show resolved Hide resolved

src/borrow_check/region_inference.md Outdated Show resolved Hide resolved

src/traits/hrtb.md Outdated Show resolved Hide resolved

src/traits/caching.md Outdated Show resolved Hide resolved

mark-i-m mentioned this pull request Oct 25, 2018

Traits chapter cleanup #219

Merged

mark-i-m and others added 4 commits October 25, 2018 11:33

Update src/borrow_check/region_inference.md

93f8731

Co-Authored-By: csmoe <[email protected]>

Update src/borrow_check/region_inference.md

6959040

Co-Authored-By: csmoe <[email protected]>

Update src/traits/hrtb.md

58106c2

Co-Authored-By: csmoe <[email protected]>

Update src/traits/caching.md

a5b90e3

Co-Authored-By: csmoe <[email protected]>

mark-i-m approved these changes Oct 25, 2018

View reviewed changes

mark-i-m merged commit 4196710 into rust-lang:master Oct 25, 2018

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Clean up skolemization with placeholder #217

Clean up skolemization with placeholder #217

csmoe commented Oct 24, 2018

mark-i-m left a comment

mark-i-m Oct 24, 2018

mark-i-m Oct 24, 2018

mark-i-m Oct 24, 2018

mark-i-m Oct 24, 2018

mark-i-m Oct 24, 2018

mark-i-m Oct 24, 2018

mark-i-m Oct 24, 2018

mark-i-m Oct 24, 2018

mark-i-m Oct 24, 2018

csmoe commented Oct 25, 2018

mark-i-m left a comment

csmoe commented Oct 25, 2018

mark-i-m commented Oct 25, 2018

	for details on placeholder, see the section
	for details on placeholders, see the section

	[placeholder and universes](#placeholder).
	[placeholders and universes](#placeholder).

	Here we would placeholer the supertype, as before, yielding:
	Here we would placeholder the supertype, as before, yielding:

Clean up skolemization with placeholder #217

Clean up skolemization with placeholder #217

Conversation

csmoe commented Oct 24, 2018

mark-i-m left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

csmoe commented Oct 25, 2018

mark-i-m left a comment

Choose a reason for hiding this comment

csmoe commented Oct 25, 2018

mark-i-m commented Oct 25, 2018