Zulip Chat Archive
Stream: triage
Topic: issue #946: data.nat.cast.cast is too general to be an in...
Random Issue Bot (Nov 26 2020 at 14:20):
Today I chose issue 946 for discussion!
data.nat.cast.cast is too general to be an instance
Created by @None (@simonjwinwood) on 2019-04-17
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Nov 26 2020 at 15:26):
Random Issue Bot (Dec 16 2020 at 14:25):
Today I chose issue 946 for discussion!
data.nat.cast.cast is too general to be an instance
Created by @None (@simonjwinwood) on 2019-04-17
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Eric Wieser (Dec 16 2020 at 14:30):
Random Issue Bot (Feb 20 2021 at 14:19):
Today I chose issue 946 for discussion!
data.nat.cast.cast is too general to be an instance
Created by @None (@simonjwinwood) on 2019-04-17
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Mar 05 2021 at 14:20):
Today I chose issue 946 for discussion!
data.nat.cast.cast is too general to be an instance
Created by @None (@simonjwinwood) on 2019-04-17
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Mar 13 2021 at 14:21):
Today I chose issue 946 for discussion!
data.nat.cast.cast is too general to be an instance
Created by @None (@simonjwinwood) on 2019-04-17
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Scott Morrison (Mar 13 2021 at 22:57):
It seems at the conclusion of #5664, which added nat.bin_cast, there was a suggestion to try making it the implementation of the coercion. Did anyone attempt this?
Scott Morrison (Mar 13 2021 at 22:58):
It seems that it would be a satisfactory resolution to this old issue!
Yakov Pechersky (Mar 14 2021 at 00:23):
Yes, I tried doing it. But too many things use nat.cast in places where there is no proof of associativity, commutativity, or '0+0=0' which is what makes nat.cast and nat.bin_cast probably equal
Yakov Pechersky (Mar 14 2021 at 00:24):
For example, it was a slog to try to get it working for pgame.short, so I abandoned the attempt.
Scott Morrison (Mar 14 2021 at 00:40):
Ah, thanks! It's nice to know the combinatorial games are a good test case for this issue.
Scott Morrison (Mar 14 2021 at 00:41):
Could we try something like "use nat.bin_cast by default, but it's okay, e.g. in pgame, to instead use the more primitive coercion"?
Yakov Pechersky (Mar 14 2021 at 00:56):
So, instance priority based add_comm_monoid -> nat.bin_cast, and nat.cast as lower priority?
Scott Morrison (Mar 14 2021 at 01:14):
Yes.
Scott Morrison (Mar 14 2021 at 01:14):
Maybe it ends up being confusing.
Random Issue Bot (Oct 30 2021 at 14:18):
Today I chose issue 946 for discussion!
data.nat.cast.cast is too general to be an instance
Created by @None (@simonjwinwood) on 2019-04-17
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC