Stream: wg-traits

Topic: coinductive all the way


nikomatsakis (Jun 11 2019 at 18:24, on Zulip):

Hey @scalexm -- so I've been wondering about whether it would be possible to make all trait matching coinductive.

nikomatsakis (Jun 11 2019 at 18:24, on Zulip):

The obvious complication here has to do with implied bounds.

nikomatsakis (Jun 11 2019 at 18:24, on Zulip):

The motivation is two-fold:

nikomatsakis (Jun 11 2019 at 18:24, on Zulip):

I think this might require us to prove "fully implemented" predicates each time we prove T: Trait

nikomatsakis (Jun 11 2019 at 18:25, on Zulip):

(which definitely means we need to rename it =)

scalexm (Jun 11 2019 at 19:04, on Zulip):

@nikomatsakis interesting

scalexm (Jun 11 2019 at 19:05, on Zulip):

I’ll think about it and try to see if we can make it work

scalexm (Jun 14 2019 at 16:08, on Zulip):

@nikomatsakis i feel like it could work if we keep the separate FromEnv / FullyImplemented setting

scalexm (Jun 14 2019 at 16:09, on Zulip):

And that we lower all bounds to FullyImplemented:

impl<T> Foo for T where T: Bar {}

// Declared(T: Foo) :- FullyImplemented(T: Bar)
scalexm (Jun 14 2019 at 16:10, on Zulip):

(Both Declared and FullyImplemented would be co-inductive, as always FullyImplemented is just a carrier traits enabling us to enumerate all the super Declared bounds on a trait)

scalexm (Jun 14 2019 at 16:12, on Zulip):

However merging FullyImplemented and FromEnv (i.e. having « true » reverse rules) is definitely not possible, i gave an example some time ago in the « alternate implied bounds lowering » stream

scalexm (Jun 14 2019 at 16:22, on Zulip):

Best thing to do would be to prototype in chalk, also I’ll have to re-spend a lot of time to convince myself this new setting is sound :)

nikomatsakis (Jun 14 2019 at 16:55, on Zulip):

before we do that

nikomatsakis (Jun 14 2019 at 16:55, on Zulip):

I have to fix the soundness bug in today's coinductive handling

nikomatsakis (Jun 14 2019 at 16:55, on Zulip):

=)

nikomatsakis (Jun 14 2019 at 16:55, on Zulip):

However merging FullyImplemented and FromEnv (i.e. having « true » reverse rules) is definitely not possible, i gave an example some time ago in the « alternate implied bounds lowering » stream

yeah I figured that the from-env/fully-impl split was the key innovation that might make this possible

nikomatsakis (Jun 24 2019 at 18:30, on Zulip):

I have to fix the soundness bug in today's coinductive handling

I guess this isn't really a blocker -- @scalexm is this something you'd be curious to play with?

nikomatsakis (Jun 24 2019 at 18:31, on Zulip):

Also, remind me, you proved the soundness of the current setup -- or sketched a proof -- or something like that, right? I was discussing the whole setup with @Aaron Turon a few days back and made an assertion like this, but I want to be sure I'm correct. =)

scalexm (Jun 24 2019 at 18:39, on Zulip):

@nikomatsakis yes i sketched a proof that the current setup was correct in the absence of implied bounds from types, although I believe they’re quite trivial to add

scalexm (Jun 24 2019 at 18:40, on Zulip):

But the proof is very simple, basically an induction on the minimal depth of a proof tree

scalexm (Jun 24 2019 at 18:41, on Zulip):

About the « coinductive all the way » setup, I could try to give it a go yeah

Aaron Hill (Aug 21 2019 at 22:40, on Zulip):

I'm interested in working on lazy normalization

Aaron Hill (Aug 21 2019 at 22:40, on Zulip):

Is that blocked on further integration of chalk?

Aaron Hill (Aug 21 2019 at 22:41, on Zulip):

Or is it something that's reasonable to work on right now?

Aaron Hill (Aug 21 2019 at 22:43, on Zulip):

@nikomatsakis eddyb suggested I ask you about this

Last update: Nov 18 2019 at 01:55UTC