From 68d30b64cf3011afc9199e3797be09ec586314c4 Mon Sep 17 00:00:00 2001 From: csmoe Date: Thu, 25 Oct 2018 11:01:08 +0800 Subject: [PATCH] replace bound region with placeholder --- src/appendix/glossary.md | 2 +- src/borrow_check/region_inference.md | 15 +++++++-------- src/traits/hrtb.md | 14 +++++++------- 3 files changed, 15 insertions(+), 16 deletions(-) diff --git a/src/appendix/glossary.md b/src/appendix/glossary.md index 04d35777..82d6f9a2 100644 --- a/src/appendix/glossary.md +++ b/src/appendix/glossary.md @@ -53,7 +53,7 @@ rib | a data structure in the name resolver that keeps trac sess | the compiler session, which stores global data used throughout compilation side tables | because the AST and HIR are immutable once created, we often carry extra information about them in the form of hashtables, indexed by the id of a particular node. sigil | like a keyword but composed entirely of non-alphanumeric tokens. For example, `&` is a sigil for references. -placeholder | a way of handling subtyping around "for-all" types (e.g., `for<'a> fn(&'a u32)`) as well as solving higher-ranked trait bounds (e.g., `for<'a> T: Trait<'a>`). See [the chapter on placeholder and universes](../borrow_check/region_inference.html#placeholder) for more details. +placeholder | **NOTE: skolemization is deprecated by placeholder** a way of handling subtyping around "for-all" types (e.g., `for<'a> fn(&'a u32)`) as well as solving higher-ranked trait bounds (e.g., `for<'a> T: Trait<'a>`). See [the chapter on placeholder and universes](../borrow_check/region_inference.html#placeholder) for more details. soundness | soundness is a technical term in type theory. Roughly, if a type system is sound, then if a program type-checks, it is type-safe; i.e. I can never (in safe rust) force a value into a variable of the wrong type. (see "completeness"). span | a location in the user's source code, used for error reporting primarily. These are like a file-name/line-number/column tuple on steroids: they carry a start/end point, and also track macro expansions and compiler desugaring. All while being packed into a few bytes (really, it's an index into a table). See the Span datatype for more. substs | the substitutions for a given generic type or item (e.g. the `i32`, `u32` in `HashMap`) diff --git a/src/borrow_check/region_inference.md b/src/borrow_check/region_inference.md index 61713300..c754a500 100644 --- a/src/borrow_check/region_inference.md +++ b/src/borrow_check/region_inference.md @@ -80,8 +80,8 @@ The kinds of region elements are as follows: to the remainder of program execution after this function returns. - There is an element `!1` for each placeholder region `!1`. This corresponds (intuitively) to some unknown set of other elements – - for details on placeholder, see the section - [placeholder and universes](#placeholder). + for details on placeholders, see the section + [placeholders and universes](#placeholder). ## Causal tracking @@ -117,7 +117,7 @@ for its argument, and `bar` wants to be given a function that that accepts **any** reference (so it can call it with something on its stack, for example). But *how* do we reject it and *why*? -### Subtyping and Placeholder +### Subtyping and Placeholders When we type-check `main`, and in particular the call `bar(foo)`, we are going to wind up with a subtyping relationship like this one: @@ -129,8 +129,7 @@ the type of `foo` the type `bar` expects ``` We handle this sort of subtyping by taking the variables that are -bound in the supertype and **placeholder** them: this means that we -replace them with +bound in the supertype and replace them with [universally quantified](../appendix/background.html#quantified) representatives, written like `!1`. We call these regions "placeholder regions" – they represent, basically, "some unknown region". @@ -198,7 +197,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 placeholder it), we will create +"enter" into this `for<'b>` (e.g., by replace it with a placeholder), we will create a child universe of the root, let's call it U1: ```text @@ -411,7 +410,7 @@ for<'a> fn(&'a u32, &'a u32) for<'b, 'c> fn(&'b u32, &'c u32) ``` -Here we would placeholer the supertype, as before, yielding: +Here we would replace the bound region in the supertype with a placeholder, as before, yielding: ```text for<'a> fn(&'a u32, &'a u32) @@ -476,7 +475,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 placeholder the supertype: +First, we replace the bound region in the supertype with a placeholder: ```text for<'a> fn(&'a u32, &'a u32) -> &'a u32 diff --git a/src/traits/hrtb.md b/src/traits/hrtb.md index 9986bbb1..b5627588 100644 --- a/src/traits/hrtb.md +++ b/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 _placeholder_. - -1. _Skolemize_ the obligation. -2. Match the impl against the placeholder obligation. +1. replace bound regions in the obligation with placeholders. +2. Match the impl against the [placeholder] obligation. 3. Check for _placeholder leaks_. +[placeholder]: ../appendix/glossary.html#appendix-c-glossary [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 -placeholder the obligation, yielding `AnyInt : Foo<&'0 isize>` (here `'0` -represents placeholder region #0). Note that we now have no quantifiers; +replace the bound region in the obligation with a placeholder, yielding +`AnyInt : Foo<&'0 isize>` (here `'0` represents placeholder region #0). +Note that we now have no quantifiers; in terms of the compiler type, this changes from a `ty::PolyTraitRef` to a `TraitRef`. We would then create the `TraitRef` from the impl, using fresh variables for it's bound regions (and thus getting @@ -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 -placeholder to `'0` and the impl trait reference is instantiated to +replaced with a placeholder `'0` and the impl trait reference is instantiated to `Foo<&'static isize>`. When we relate those two, we get a constraint like `'static == '0`. This means that the taint set for `'0` is `{'0, 'static}`, which fails the leak check.