Stream: t-compiler/help

Topic: Universes vs Debruijn Indices


Declan Kelly (May 08 2019 at 21:26, on Zulip):

Hello, can anyone explain the differences between universes and debruijn indices? Superficially it seems that they play similar roles, counting up from a binder.

Declan Kelly (May 08 2019 at 21:33, on Zulip):

My initial thought is that debruijn indices represent quantification inside of a type, while the universes can represent quantification spanning multiple types, such as inside of an impl block.

Declan Kelly (May 09 2019 at 05:41, on Zulip):

Also how does the use of bounds vars play into this? From the TyKind docs I see that placeholder types are a Placeholder<BoundVar> where Placeholder contains a UniverseIndex. What kind of data is BoundVar associated with, and in what context is TyKind::Placeholder used? Would it just be the T in fn identity<T>(data: T) -> T {}?

tmandry (May 09 2019 at 22:00, on Zulip):

@Declan Kelly you might want to read Placeholders and universes in the rustc guide

tmandry (May 09 2019 at 22:04, on Zulip):

see also the docs on RegionKind

tmandry (May 09 2019 at 22:08, on Zulip):

I have a hard time keeping all these straight myself, though :)

tmandry (May 09 2019 at 22:10, on Zulip):

I believe the T in your example would be a BoundVar, whereas universes are used to represent quantifiers (like for<'a> in for<'a> fn (&'a u32))

tmandry (May 09 2019 at 22:10, on Zulip):

cc @nikomatsakis

Declan Kelly (May 10 2019 at 00:24, on Zulip):

@tmandry Thank you for the help!

nikomatsakis (May 13 2019 at 17:46, on Zulip):

The distinction is a matter of "point of view". When you are looking at some term (i.e., a type, where-clause, etc), it may have bound regions:

for<'a> T: Foo<'a>

Here, 'a would be represented with a debruijn index. But when we "enter" into that binder, we have to replace the bound region ('a) with something. We would replace 'a with a placeholder that has a universe (say !1). In that case, we have T: Foo<!1> as our term

Last update: Nov 11 2019 at 23:20UTC