Stream: t-compiler/wg-nll

Topic: Region inference


blitzerr (Oct 19 2018 at 03:22, on Zulip):

From the rustc-guide, can someone explain to me in this example:
for<'a> fn(&'a u32, &'a u32) -> &'a u32 <: fn(&'!1 u32, &'!2 u32) -> &'!1 u32

How this happens,
&'!1 u32 <: &'?3 u32 // arg 1 (makes sense) &'!2 u32 <: &'?3 u32 // arg 2 (makes sense) &'?3 u32 <: &'!1 u32 // return type (doesn't make sense, unless we say they are subtypes)

The last line that is for the return type, is
&'?3 u32 <: &'!1 u32 // return type
and NOT
&'!1 u32 <: &'?3 u32 // return type

blitzerr (Oct 19 2018 at 03:24, on Zulip):

And this one
V1 in U1 = {skol(1)} V2 in U2 = {skol(2)} V3 in U2 = {}

Why is V3 in U2 and not in U1 ?

csmoe (Oct 19 2018 at 11:25, on Zulip):

this difference between arg1/2 and return type caused by fn(T) -> U is contravariant over T, but covariant over U

csmoe (Oct 19 2018 at 11:25, on Zulip):

@blitzerr cc https://doc.rust-lang.org/nomicon/subtyping.html#variance

csmoe (Oct 19 2018 at 11:40, on Zulip):

btw, @nikomatsakis it seems you had cleared skolemize with placeholder in rustc, should that be apply to rustc-guide?
and function is covariant over its return type should be mentioned in this example as arguments.

nikomatsakis (Oct 19 2018 at 11:40, on Zulip):

@csmoe yep that should be applied to rustc-guide

blitzerr (Oct 19 2018 at 12:12, on Zulip):

Thanks @csmoe that doc does explain the first part. But I still don't get this one. Why is V3 working with U2 and not U1 ?

V1 in U1 = {skol(1)} V2 in U2 = {skol(2)} V3 in U2 = {}

Why is V3 in U2 and not in U1 ?

csmoe (Oct 19 2018 at 13:03, on Zulip):

@blitzerr sorry, this ques'n is beyond my knowledge, maybe you can refer to @nikomatsakis

nikomatsakis (Oct 19 2018 at 13:28, on Zulip):

@blitzerr the subtyping algorithm instantiates the binders in the subtype as existentials in some universe that can name all the things in the super type

nikomatsakis (Oct 19 2018 at 13:28, on Zulip):

one way to think about it is this:

nikomatsakis (Oct 19 2018 at 13:28, on Zulip):

if you have for<A> T <: for<B> U (in general...)

nikomatsakis (Oct 19 2018 at 13:29, on Zulip):

that is true if forall<B> { exists<A> { T <: U } }

nikomatsakis (Oct 19 2018 at 13:29, on Zulip):

that is, if "for all lifetimes B", whatever they are, there exists some lifetimes A, such that T <: U

nikomatsakis (Oct 19 2018 at 13:29, on Zulip):

the reason for this is: we have a value of the subtype (T)

nikomatsakis (Oct 19 2018 at 13:29, on Zulip):

we are storing it into a slot that is typed with the supertype (U)

nikomatsakis (Oct 19 2018 at 13:30, on Zulip):

so we have to be sure that the subtype is an instance of the supertype

nikomatsakis (Oct 19 2018 at 13:30, on Zulip):

to use a concrete example, if you had

nikomatsakis (Oct 19 2018 at 13:30, on Zulip):

for<'a> fn(&'a u32) <: fn(&'static u32)

nikomatsakis (Oct 19 2018 at 13:30, on Zulip):

that should be true, because on the one hand we have a fn that accepts any region

nikomatsakis (Oct 19 2018 at 13:31, on Zulip):

and we are using it in a spot where it will only have to accept the static region

nikomatsakis (Oct 19 2018 at 13:31, on Zulip):

since the static region is a region, that should be fine

nikomatsakis (Oct 19 2018 at 13:31, on Zulip):

(but the reverse is not true -- if the fn only accepts 'static, it cannot be used in a spot where it maybe given anything)

nikomatsakis (Oct 19 2018 at 13:32, on Zulip):

since the static region is a region, that should be fine

expressed the way I put it before:

forall<> { exists<'a> { fn(&'a u32) <: fn(&'static u32) } }

nikomatsakis (Oct 19 2018 at 13:32, on Zulip):

the outer forall is empty because the supertype here doesn't have any bound regions

blitzerr (Oct 19 2018 at 13:59, on Zulip):

Thanks @nikomatsakis that makes sense. How do we read “<:” ?

pnkfelix (Oct 19 2018 at 14:05, on Zulip):

you mean how is <: pronounced?

pnkfelix (Oct 19 2018 at 14:06, on Zulip):

S <: T, for types S and T, is usually pronounced "S is a subtype of T"

blitzerr (Oct 19 2018 at 14:06, on Zulip):

Right

pnkfelix (Oct 19 2018 at 14:07, on Zulip):

e.g. https://en.wikipedia.org/wiki/Subtyping

blitzerr (Oct 19 2018 at 14:07, on Zulip):

Ahh Subtype, I was thinking sunset.

nikomatsakis (Oct 19 2018 at 14:07, on Zulip):

there's a relationship :)

blitzerr (Oct 19 2018 at 14:07, on Zulip):

Thanks @pnkfelix

nikomatsakis (Oct 19 2018 at 14:07, on Zulip):

i.e., the set of values with type T is a subset of those with type U, if T <: U

pnkfelix (Oct 19 2018 at 14:08, on Zulip):

oh oh, subset

pnkfelix (Oct 19 2018 at 14:08, on Zulip):

/me was super confused

nikomatsakis (Oct 19 2018 at 14:08, on Zulip):

to the tune of "sunrise, subset"... "super-subset"

blitzerr (Oct 19 2018 at 14:09, on Zulip):

Subtype*. This autocorrect :grinning:

blitzerr (Oct 19 2018 at 14:37, on Zulip):

Thanks a lot @nikomatsakis and @pnkfelix

blitzerr (Oct 19 2018 at 15:15, on Zulip):

I am traveling and on way to somewhere but after I read up on all this, will post further questions if I had any. Thanks @csmoe @nikomatsakis and @pnkfelix for clarifications.

blitzerr (Oct 19 2018 at 15:16, on Zulip):

And sorry for the /subset/sunset/ confusion. :joy:

pnkfelix (Oct 19 2018 at 15:18, on Zulip):

i love staring for hours at a good subset

blitzerr (Oct 19 2018 at 15:34, on Zulip):

Usually with some wine :ok:

blitzerr (Oct 19 2018 at 15:34, on Zulip):

I have always liked every subset I have met :wink:

Last update: Nov 21 2019 at 13:50UTC