Stream: wg-traits

Topic: 2020 sprint 1


Jack Huey (Feb 12 2020 at 15:14, on Zulip):

I decided it would be better to have a stream specifically dedicated to the topic, rather than extending the design meeting topic

Jack Huey (Feb 12 2020 at 15:15, on Zulip):

@nikomatsakis @detrumi @Aaron Hill @David Barsky @Jane Lusby @matprec

Jack Huey (Feb 12 2020 at 15:15, on Zulip):

link to sprint doc for future reference: https://paper.dropbox.com/doc/wg-traits-2020-sprint-planning--AuNFr3WGUhJ~DsCkt_aNOxmvAg-SSt74TfcovdnKKhZNyzeW

Jane Lusby (Feb 12 2020 at 16:11, on Zulip):

:+1:

Jack Huey (Feb 12 2020 at 16:12, on Zulip):

@Jane Lusby if you're interested in adding tracing support, @David Barsky is also helping with that

Jack Huey (Feb 12 2020 at 16:13, on Zulip):

But I'm not entirely sure how much progress he's made on Chalk

Jane Lusby (Feb 12 2020 at 16:13, on Zulip):

I'll ask him

Jack Huey (Feb 12 2020 at 16:14, on Zulip):

I know he's been working on his library

David Barsky (Feb 12 2020 at 16:14, on Zulip):

heya jane

Jack Huey (Feb 12 2020 at 16:14, on Zulip):

more discussion in https://rust-lang.zulipchat.com/#narrow/stream/144729-wg-traits/topic/tracing.20in.20chalk

Jack Huey (Feb 12 2020 at 16:19, on Zulip):

Also @detrumi and @nikomatsakis, in regards to exporting a lowered program/goals to a .chalk file (since I did a little bit a week or two ago):

Jack Huey (Feb 12 2020 at 16:19, on Zulip):

I think the big blocking thing there (or at least the first blocking thing) is actually having some "context" when printing binders

Jack Huey (Feb 12 2020 at 16:20, on Zulip):

So trait impls can be printed correctly

Jack Huey (Feb 12 2020 at 16:20, on Zulip):

(i.e. a name like T instead of ^0)

Jack Huey (Feb 12 2020 at 16:21, on Zulip):

it would be interesting to think about how much (if any) this overlaps with: https://github.com/rust-lang/chalk/issues/287

Florian Diebold (Feb 12 2020 at 16:31, on Zulip):

(i.e. a name like T instead of ^0)

couldn't you substitute the variables for placeholders that print nicely at the point where the binders are introduced? i.e. when you're printing the impl. That's what RA does in a similar situation

Jack Huey (Feb 12 2020 at 16:33, on Zulip):

can you be a bit more clear?

Jack Huey (Feb 12 2020 at 16:34, on Zulip):

so, the problem is trying to print something like impl<'a, T> Trait<T> for Struct<'a>

Jack Huey (Feb 12 2020 at 16:36, on Zulip):

That stored in the Program as essentially forall<^'0, ^1> Trait<Struct<^'0>, ^1>

Jack Huey (Feb 12 2020 at 16:38, on Zulip):

the tough part is actually propagating the named binders through the bound type

Jack Huey (Feb 12 2020 at 16:39, on Zulip):

I was trying to think of a way to reuse the existing debug/display infra as best as possible

Florian Diebold (Feb 12 2020 at 16:39, on Zulip):

basically, I imagine there's something like format!("impl {} for {}", trait, type) somewhere, and you could do type.subst(^0 -> T) at that point (pseudocode, obviously). I.e. in the place where you are printing the whole impl, you have the binders and can give names to each one, and then substitute them into the types before printing them. That only works if you can represent the T as a placeholder that prints like that, of course

Jack Huey (Feb 12 2020 at 16:40, on Zulip):

yeah, I think what you're suggesting is similar to what I'm thinking

Jack Huey (Feb 12 2020 at 16:42, on Zulip):

and you could do type.subst(^0 -> T) at that point (pseudocode, obviously). I.e. in the place where you are printing the whole impl

This is similar to what I was thinking. We already have the TF:: debug* functions that existing Debug impls call for some things. Just need add one for bound variables and track as new binders are added

Florian Diebold (Feb 12 2020 at 16:51, on Zulip):

what I mean is that in RA there's an actual type that already prints as T, so we can just use normal type substitution to replace the bound variables by those placeholder types, and then it prints nicely. it might be a bit more complicated in Chalk

Jack Huey (Feb 12 2020 at 16:56, on Zulip):

Ohh, I see

Jack Huey (Feb 12 2020 at 16:56, on Zulip):

That's an interesting idea

detrumi (Feb 18 2020 at 12:59, on Zulip):

We didn't talk about dates at all. If we consider the sprint as 'started' on Feb 11, then 6 weeks later would be around March 24

Jack Huey (Feb 19 2020 at 00:50, on Zulip):

@detrumi thanks for bringing this up. good to keep in mind

nikomatsakis (Feb 24 2020 at 17:41, on Zulip):

Yep, thanks

Last update: Feb 25 2020 at 04:25UTC