Stream: wg-traits

Topic: re. coherence


centril (Apr 25 2019 at 16:24, on Zulip):

/me mulls replacing "coherence" with "canonicity" since that's probably more accurate

csmoe (Apr 25 2019 at 16:26, on Zulip):

(@centril sorry for cutting in, is there any open materials about rust coherence? rfc, paper etc)

centril (Apr 25 2019 at 16:28, on Zulip):

@csmoe you may want to start with http://blog.ezyang.com/2014/07/type-classes-confluence-coherence-global-uniqueness/

rfcs include:
- https://github.com/rust-lang/rfcs/pull/2451

this links to a bunch of other places

centril (Apr 25 2019 at 16:28, on Zulip):

I suspect most papers about coherence are in a Haskell setting

csmoe (Apr 25 2019 at 16:29, on Zulip):

@centril really thanks :slight_smile:

centril (Apr 25 2019 at 16:29, on Zulip):

Rust enforces canonicity, which is a stronger property than coherence

centril (Apr 25 2019 at 16:29, on Zulip):

canonicity being the same as "global uniqueness of implementations"

centril (Apr 25 2019 at 16:30, on Zulip):

@csmoe welcome!

centril (Apr 25 2019 at 16:34, on Zulip):

@csmoe if you are familiar with the concept of proof relevance... if we consider a trait to be a proposition and an implementation of a trait for a given type to be a witness / proof of said proposition, then canonicity can be seen as proof irrelevance

detrumi (Apr 25 2019 at 16:34, on Zulip):

Oh cool, so Rust basically does the same thing as Haskell (without OverlappingInstancesand IncoherentInstances)

centril (Apr 25 2019 at 16:35, on Zulip):

@detrumi and no orphans as well :slight_smile:

detrumi (Apr 25 2019 at 16:36, on Zulip):

/me is pleasantly surprised to find so many Haskell ideas in Rust :slight_smile:

centril (Apr 25 2019 at 16:37, on Zulip):

@detrumi other than that, the basic idea is the same but how it is achieved is likely different; "coherence" is a Haskell term after all ^^

detrumi (Apr 25 2019 at 16:38, on Zulip):

"is likely different", what does that mean?

csmoe (Apr 25 2019 at 16:39, on Zulip):

@centril know nothing :joy: I need to understand the docs you gave first.

centril (Apr 25 2019 at 16:40, on Zulip):

@detrumi the mechanism you use to prevent overlapping instances doesn't have to be the same

detrumi (Apr 25 2019 at 16:40, on Zulip):

Ah, in that sense

Last update: Nov 12 2019 at 16:05UTC