Stream: wg-traits

Topic: meeting 2019-10-16


nikomatsakis (Oct 16 2019 at 18:06, on Zulip):

Oh hai @WG-traits -- so this week has sort of been a mess, but let's try to have some sort of design meeting anyway!

nikomatsakis (Oct 16 2019 at 18:06, on Zulip):

Couple of things:

nikomatsakis (Oct 16 2019 at 18:06, on Zulip):

I won't be able to do this time after all

nikomatsakis (Oct 16 2019 at 18:07, on Zulip):

I think Monday would work better for me

nikomatsakis (Oct 16 2019 at 18:07, on Zulip):

Though I might be able to do a different time on Wednesday

nikomatsakis (Oct 16 2019 at 18:07, on Zulip):

The question is -- what should we talk about -- I had hope to have a bit of a "presentation" on this, but as I said, this week has had a lot of last minute things coming up and I have just not had time.

nikomatsakis (Oct 16 2019 at 18:07, on Zulip):

But let me float some of the things on my mind :)

nikomatsakis (Oct 16 2019 at 18:08, on Zulip):
nikomatsakis (Oct 16 2019 at 18:09, on Zulip):
nikomatsakis (Oct 16 2019 at 18:09, on Zulip):
nikomatsakis (Oct 16 2019 at 18:10, on Zulip):
nikomatsakis (Oct 16 2019 at 18:10, on Zulip):

I guess the root question is "chalk or rustc"?

nikomatsakis (Oct 16 2019 at 18:10, on Zulip):

Given the folks who :wave:'d above, maybe chalk?

nikomatsakis (Oct 16 2019 at 18:10, on Zulip):

(In the future, I'd like to pick topics for next time ahead of time)

nikomatsakis (Oct 16 2019 at 18:11, on Zulip):

also, here is a hackmd for taking notes and the like

tmandry (Oct 16 2019 at 18:11, on Zulip):

I think extracting a shared type library would be really interesting, sounds challenging though

tmandry (Oct 16 2019 at 18:11, on Zulip):

Oops, wrong topic

nikomatsakis (Oct 16 2019 at 18:11, on Zulip):

oh wait

nikomatsakis (Oct 16 2019 at 18:12, on Zulip):

did I just mergr those two topics completely

nikomatsakis (Oct 16 2019 at 18:12, on Zulip):

dang it :)

nikomatsakis (Oct 16 2019 at 18:12, on Zulip):

oh, no, I didn't, shew

nikomatsakis (Oct 16 2019 at 18:12, on Zulip):

Oops, wrong topic

yeah I retopic'd :)

nikomatsakis (Oct 16 2019 at 18:12, on Zulip):

ok, well, let's talk about "shared type libary" and "changing how types are represented in chalk"

nikomatsakis (Oct 16 2019 at 18:12, on Zulip):

they kind of overlap

nikomatsakis (Oct 16 2019 at 18:12, on Zulip):

let me just lay out a few strands to start

nikomatsakis (Oct 16 2019 at 18:13, on Zulip):

one of the things I would like to do is to change how we handle normalization and unifiation in chalk

nikomatsakis (Oct 16 2019 at 18:13, on Zulip):

right now, we have a type that represents an "unnormalized trait projection", like <T as Iterator>::Item

nikomatsakis (Oct 16 2019 at 18:13, on Zulip):

our unification logic understands what this means

nikomatsakis (Oct 16 2019 at 18:14, on Zulip):

so if we try to unify <T as Iterator>::Item with some other type U, that "always succeeds", but it generates a pending obligation of the form ProjectionEq(<T as Iterator>::Item = U)

nikomatsakis (Oct 16 2019 at 18:14, on Zulip):

that notation is maybe a touch confusing -- but basically the idea is that you have to prove that <T as Iterator>::Item can be 'normalized to U` based on the impls around

nikomatsakis (Oct 16 2019 at 18:15, on Zulip):

this is sort of a weird special case since most of unify is about proving that two types are syntactically equal (well, modulo regions)

nikomatsakis (Oct 16 2019 at 18:15, on Zulip):

it's also a bit of a divergence from "prolog", where unification is all about syntactic equality

nikomatsakis (Oct 16 2019 at 18:15, on Zulip):

(make sense so far?)

nikomatsakis (Oct 16 2019 at 18:16, on Zulip):

so why do I care?

nikomatsakis (Oct 16 2019 at 18:16, on Zulip):

well, for one thing, I want to lower as much as possible to something that resembles a simple prolog-liek thing

nikomatsakis (Oct 16 2019 at 18:17, on Zulip):

but also if we have an impl like this one:

nikomatsakis (Oct 16 2019 at 18:17, on Zulip):
impl<T> Foo for T::Item { .. }
nikomatsakis (Oct 16 2019 at 18:17, on Zulip):

er, that's not the problem, sorry

nikomatsakis (Oct 16 2019 at 18:17, on Zulip):

well, if you're trying to prove a goal like Implemented(<T as Iterator>::Item) --

nikomatsakis (Oct 16 2019 at 18:17, on Zulip):

(where that is not normalized)

nikomatsakis (Oct 16 2019 at 18:18, on Zulip):

sorry, maybe Implemented(<T as Iterator>::Item: Foo)

nikomatsakis (Oct 16 2019 at 18:18, on Zulip):

anyway you have no idea what the self type is

nikomatsakis (Oct 16 2019 at 18:18, on Zulip):

beacuse it unifies with anything

nikomatsakis (Oct 16 2019 at 18:18, on Zulip):

but likely it is quite a bit more constrained than that :)

nikomatsakis (Oct 16 2019 at 18:18, on Zulip):

we are currently floundering if we have a goal like Implemented(?X: Foo) -- i.e., where self-type is fully unknown

nikomatsakis (Oct 16 2019 at 18:18, on Zulip):

anyway so what I would like to do is to remove "unnormalized" projections

nikomatsakis (Oct 16 2019 at 18:18, on Zulip):

as a type

nikomatsakis (Oct 16 2019 at 18:19, on Zulip):

and instead just have "placeholder" ones -- actually kind of like rustc in this regard

nikomatsakis (Oct 16 2019 at 18:19, on Zulip):

but I'd like to move that normalization to the lowering phase

nikomatsakis (Oct 16 2019 at 18:19, on Zulip):

so if we have

impl<T: Iterator> Foo for T::Item { .. }
nikomatsakis (Oct 16 2019 at 18:19, on Zulip):

today we would generate a lowered rule like

forall<T: Iterator> {
    Implemented(<T as Iterator>::Item: Foo)
}
nikomatsakis (Oct 16 2019 at 18:20, on Zulip):

and instead just have "placeholder" ones -- actually kind of like rustc in this regard

(I'll use the notation (Iterator::Item)<T> for those, since that is what we use in chalk)

nikomatsakis (Oct 16 2019 at 18:20, on Zulip):

I'd prefer to generate this rule

nikomatsakis (Oct 16 2019 at 18:20, on Zulip):
forall<T: Iterator, U> {
    Implemented(U: Foo) :-
        ProjectionEq(<T as Iterator>::Item = U)
}
nikomatsakis (Oct 16 2019 at 18:21, on Zulip):

in a sense I've just "unrolled" what unification would have done anyway

nikomatsakis (Oct 16 2019 at 18:21, on Zulip):

(does that make sense?)

tmandry (Oct 16 2019 at 18:22, on Zulip):

my impression is that this wasn’t done in the first place because it made the rules less ergonomic, is that right?

nikomatsakis (Oct 16 2019 at 18:23, on Zulip):

yeah, so, I've thought about it before; it obviously moves the lowered form a bit farther from Rust surface syntax

nikomatsakis (Oct 16 2019 at 18:23, on Zulip):

it's also just kind of a bit of a pain to implement with the system as it is

nikomatsakis (Oct 16 2019 at 18:23, on Zulip):

(which is part of what connects this to a shared type libary)

nikomatsakis (Oct 16 2019 at 18:23, on Zulip):

in particular, the user basically writes types that include unnormalized projections

nikomatsakis (Oct 16 2019 at 18:24, on Zulip):

today, we can kind of lower the user's types and embed them directly into the final rules -- actually, in the clause generating code, the "types" from user are chalk_ir::Ty

nikomatsakis (Oct 16 2019 at 18:24, on Zulip):

so we can literally just embed them into the clauses we build

nikomatsakis (Oct 16 2019 at 18:25, on Zulip):

but what we have to do now is to say "if this type is an unnormalizd projection, instead we generate a fresh variable and some new clauses" etc

nikomatsakis (Oct 16 2019 at 18:25, on Zulip):

it's not hard per se but it's a bit more complex than before

nikomatsakis (Oct 16 2019 at 18:25, on Zulip):

but I'm not very happy with the clause generator code anyway

nikomatsakis (Oct 16 2019 at 18:25, on Zulip):

it's super opaque, particularly around debruijn binders, and I think nobody gets it

nikomatsakis (Oct 16 2019 at 18:25, on Zulip):

so what I was thinking is this

nikomatsakis (Oct 16 2019 at 18:26, on Zulip):

first off, it seems like we sort of want two concepts of types

nikomatsakis (Oct 16 2019 at 18:26, on Zulip):

"pre-lowering" (which only includes unnormalized projections)

nikomatsakis (Oct 16 2019 at 18:26, on Zulip):

"clauses" (which never does)

nikomatsakis (Oct 16 2019 at 18:27, on Zulip):

at least conceptually we want that

nikomatsakis (Oct 16 2019 at 18:27, on Zulip):

and converting between the two is something you have to do carefully

nikomatsakis (Oct 16 2019 at 18:27, on Zulip):

I'd like to use generic types for this, I think

tmandry (Oct 16 2019 at 18:29, on Zulip):

so, in a sense, we're moving the complexity of these unnormalized projections out of unification and into the "pre-lowering => clauses" step?

nikomatsakis (Oct 16 2019 at 18:29, on Zulip):

so that we hvae some generic type T: RustType or something -- and some operations to (e.g.) figure out which variant of rust type it is. Probably there is a little "family"

trait RustTypeFamily {
    type Type;
    type Substitutions;

    fn variant(Self::Type) -> TypeVariants<F>;
}

enum TypeVariants<F: RustTypeFamily> {
    Apply(AppicationTy, F::Substitutions)
}
nikomatsakis (Oct 16 2019 at 18:29, on Zulip):

so, in a sense, we're moving the complexity of these unnormalized projections out of unification and into the "pre-lowering => clauses" step?

yes, exactly

nikomatsakis (Oct 16 2019 at 18:29, on Zulip):

there are a few reasons to use generics

nikomatsakis (Oct 16 2019 at 18:29, on Zulip):

but one of them that is nice is that

nikomatsakis (Oct 16 2019 at 18:30, on Zulip):

it might be that both the "before" and "after" types are represented by the same thing

nikomatsakis (Oct 16 2019 at 18:30, on Zulip):

but the semantics (particularly of projections!) are different

nikomatsakis (Oct 16 2019 at 18:30, on Zulip):

and if they have different generic types, then compiler can help us keep them separated

nikomatsakis (Oct 16 2019 at 18:30, on Zulip):

in particular, when we lower from a BeforeType to an AfterType, if it is a projection, we can generate the clauses we need

nikomatsakis (Oct 16 2019 at 18:31, on Zulip):

i.e., there'd be something like

fn lower_type(before: &Before::Type, obligations: &mut Vec<Goal>) -> After::Type
nikomatsakis (Oct 16 2019 at 18:31, on Zulip):

so now if I see a projection, I can generate the ProjectionEq(...) goal and push it onto obligations

nikomatsakis (Oct 16 2019 at 18:31, on Zulip):

this is exactly what unify used to be doing at runtime

nikomatsakis (Oct 16 2019 at 18:32, on Zulip):

but we're doing it at clause generation time

nikomatsakis (Oct 16 2019 at 18:32, on Zulip):

/me pauses to see if folks have questions

nikomatsakis (Oct 16 2019 at 18:34, on Zulip):

ok

tmandry (Oct 16 2019 at 18:34, on Zulip):

/me typing

nikomatsakis (Oct 16 2019 at 18:34, on Zulip):

heh :)

nikomatsakis (Oct 16 2019 at 18:34, on Zulip):

/me waits more

tmandry (Oct 16 2019 at 18:34, on Zulip):

what you just said makes sense. just to build on my summary from before... the reason for moving all of this out of unification is so that we don't encounter so much complexity with regards to clause/goal selection and floundering?

nikomatsakis (Oct 16 2019 at 18:35, on Zulip):

yes, I have a few motivations

nikomatsakis (Oct 16 2019 at 18:35, on Zulip):

that is one of them

nikomatsakis (Oct 16 2019 at 18:35, on Zulip):

I also want to try and align our "lowered representation" with something that is closer to prolog because -- long term -- I want to make some kind of virtual machine to efficiently execute this stuff

nikomatsakis (Oct 16 2019 at 18:36, on Zulip):

and if unification looks more like "syntactic equality" and less like "a mini interpreter", that will be easier

nikomatsakis (Oct 16 2019 at 18:37, on Zulip):

another reason is that I think it should be a touch more efficient, and it's also maybe a better strategy long term for managing projections -- I'm not sure how true this , I guess. There are some other issues around the normalization strategy that chalk is using that suggests we may want to try to have some kind of "normalization function" more like what rust does --

tmandry (Oct 16 2019 at 18:38, on Zulip):

/me is taking off and might not be as responsive, fyi

nikomatsakis (Oct 16 2019 at 18:38, on Zulip):

I guess I think that any such changes will be easier if we separate out the "projection-eq" part more cleanly, so that types are simpler

nikomatsakis (Oct 16 2019 at 18:38, on Zulip):

anyway, the connection that all this has to a "generic definition fo types" that can be shared is

nikomatsakis (Oct 16 2019 at 18:38, on Zulip):

well, I already started to give you what one might look like

nikomatsakis (Oct 16 2019 at 18:38, on Zulip):

so that we hvae some generic type T: RustType or something -- and some operations to (e.g.) figure out which variant of rust type it is. Probably there is a little "family"

trait RustTypeFamily {
    type Type;
    type Substitutions;

    fn variant(Self::Type) -> TypeVariants<F>;
}

enum TypeVariants<F: RustTypeFamily> {
    Apply(AppicationTy, F::Substitutions)
}
nikomatsakis (Oct 16 2019 at 18:39, on Zulip):

so in this case we are not specifying the structures per se but rather a kind of trait

nikomatsakis (Oct 16 2019 at 18:39, on Zulip):

we'll need a few more operations (e.g., to "intern")

nikomatsakis (Oct 16 2019 at 18:39, on Zulip):

I have to do a bit of work to define that trait, what I wrote up there isn't quite it, there is a bit more

nikomatsakis (Oct 16 2019 at 18:39, on Zulip):

notably I thikn it's generic over the ApplicationTy, for example

nikomatsakis (Oct 16 2019 at 18:39, on Zulip):

but then I think we can implement this for Rust and have the type (internally) be Ty<'tcx>

nikomatsakis (Oct 16 2019 at 18:40, on Zulip):

and rust-analyzer can implement it and have types be "whatever"

nikomatsakis (Oct 16 2019 at 18:40, on Zulip):

and we can make all the logic in chalk-solve and friends kind of generic over that

nikomatsakis (Oct 16 2019 at 18:40, on Zulip):

I was hoping to start playing with this before the meeting but .. yeah .. life

nikomatsakis (Oct 16 2019 at 18:41, on Zulip):

I think though that chalk's "core variants" are probably about right, though we may want to tweak how they are structured

nikomatsakis (Oct 16 2019 at 18:41, on Zulip):

note also that the variant method can "convert" on the fly from rustc's Ty representation to a chalk one, at least at first -- probably we'd want them to match up as closely as possibly eventually

nikomatsakis (Oct 16 2019 at 18:42, on Zulip):

some random thoughts that I've been wondering about:

nikomatsakis (Oct 16 2019 at 18:42, on Zulip):

debruijn or not?

nikomatsakis (Oct 16 2019 at 18:43, on Zulip):

I love me some debruijn indices but .. they're also kind of confusing. Maybe it'd be better to just use "uuids" or something for each binding spot? (And disallow shadowing) In particular I think we could make the clause generation stuff a lot more ergonomic

nikomatsakis (Oct 16 2019 at 18:43, on Zulip):

how would we actually implement this transition is another good question

nikomatsakis (Oct 16 2019 at 18:44, on Zulip):

I have to think about the exact steps but I guess the right way to start would be to try and introduce a trait first, making things more and more generic over said trait, but keeping the same underlying types

nikomatsakis (Oct 16 2019 at 18:45, on Zulip):

but this all feels like stuff that's a bit hard to dig into in the abstract

nikomatsakis (Oct 16 2019 at 18:45, on Zulip):

easier with an open editor :)

nikomatsakis (Oct 16 2019 at 18:45, on Zulip):

I'd definitely keep the debruijin setup until the rest is in place, I guess, but it defintiely affects the generic "type family" sort of operations, as you'll need to have notions of shifting and what not --

nikomatsakis (Oct 16 2019 at 18:46, on Zulip):

that said, if we use generics -- we might be abel to make it a compilation time error to forget to shift :)

nikomatsakis (Oct 16 2019 at 18:47, on Zulip):

ok, that's about all I've got I guess :) I'll stop here but this is something I really want to start experimenting with asap to "try out". I don't plan to do all the work myself, I'd like to do enough of the steps I'm convinced it will work and then work with someone else (or maybe work with someone else a bit from the start)

tmandry (Oct 16 2019 at 18:52, on Zulip):

re: deBruijn indices the shifting is quite subtle, but if we moved away from it I’d be concerned about performance. Maybe we can introduce some nice abstractions around this, as you mentioned

nikomatsakis (Oct 16 2019 at 18:53, on Zulip):

yeah that's really a separate topic

nikomatsakis (Oct 16 2019 at 18:53, on Zulip):

Both have their performance issues

tmandry (Oct 16 2019 at 18:57, on Zulip):

I’m also curious what we’ve learned about the different concrete type representations you’d want in rustc vs rust-analyzer. Like I know that rustc types are pretty coupled to the internals, but not sure if it has to be that way.

In other words, are generics over type representations the way we would do it if we were starting over, or a way of making migration more feasible?

nikomatsakis (Oct 16 2019 at 18:58, on Zulip):

Some of both

nikomatsakis (Oct 16 2019 at 18:58, on Zulip):

The pros I see is precisely the ability to make these syntactic distinctions

nikomatsakis (Oct 16 2019 at 18:58, on Zulip):

These come up in rustc too, and we've just opted not to have the extra static safety

nikomatsakis (Oct 16 2019 at 18:59, on Zulip):

On the other hand, it does induce some amount of "forced inefficiency" because you can't assume the types are the same, even if you happen to know that (in some particular case) you just want the same type

nikomatsakis (Oct 16 2019 at 18:59, on Zulip):

But I think overall we do an awful amoutn of type folding and "re-interning" in rustc anyway :)

nikomatsakis (Oct 16 2019 at 19:00, on Zulip):

I think what'd I'd prefer is to have the generic layer, and then try to use specialization and/or other tricks to optimize it out where we can

nikomatsakis (Oct 16 2019 at 19:00, on Zulip):

These come up in rustc too, and we've just opted not to have the extra static safety

an example:

nikomatsakis (Oct 16 2019 at 19:00, on Zulip):

failure to do those substitutions is a common source of ICEs

nikomatsakis (Oct 16 2019 at 19:01, on Zulip):

for that matter, normalization in rustc must also be done at this time, and failure to do that is also a common problem :)

nikomatsakis (Oct 16 2019 at 19:02, on Zulip):

it seems to me that having multipe generic types that (when instantiated) wind up sharing the same representation might actually be a kind of "sweet spot"

tmandry (Oct 16 2019 at 19:09, on Zulip):

Yeah I like that idea, in theory at least :slight_smile:

Last update: Nov 18 2019 at 00:40UTC