Zulip Chat Archive

Stream: general

Topic: Coercions on subtypes


view this post on Zulip Eric Wieser (Aug 13 2020 at 17:38):

Are the has_coes in this message safe? Are they sensible? Would they make sense in mathlib?

Eric Wieser said:

This seems to work:

import data.set.basic

instance coe_left_inter {X : Type*} {A B : set X} : has_coe (A  B) A :=  λ x, x.1, set.inter_subset_left _ _ x.2 
instance coe_right_inter {X : Type*} {A B : set X} : has_coe (A  B) B :=  λ x, x.1, set.inter_subset_right _ _ x.2 

example {X Y : Type*} {A B : set X} (f : A  Y) (g: B  Y) (h :  x : A  B, f x = g x) : sorry  := sorry

view this post on Zulip Kenny Lau (Aug 13 2020 at 17:39):

nooo u can't just make every function a coercion

view this post on Zulip Reid Barton (Aug 13 2020 at 17:40):

As far as coercions go they seem pretty safe/sensible to me, since the type gets smaller and you're not generally likely to have terms of A ∩ B in the first place. Also, the instances are defeq to each other when A and B are.

view this post on Zulip Eric Wieser (Aug 13 2020 at 17:44):

since the type gets smaller

Does that then mean that has_coe ↥A ↥(A ∪ B) would _not_ be sensible / safe?

view this post on Zulip Reid Barton (Aug 13 2020 at 17:45):

it's definitely scarier

view this post on Zulip Kenny Lau (Aug 13 2020 at 17:46):

I thought the former would be scarier

view this post on Zulip Mario Carneiro (Aug 13 2020 at 18:14):

please no. The typeclass problem for coercion already includes a ton of random garbage

view this post on Zulip Reid Barton (Aug 13 2020 at 18:41):

Maybe I have the wrong mental model for how coercion instance search works? I thought it was basically directed by the actual type of the thing being coerced, and then recursive on the result of the has_coe. So instances like these are basically working by structural recursion, and won't match anything that's not of the form A ∩ B.

view this post on Zulip Rob Lewis (Aug 13 2020 at 18:50):

I think weird coercions are a great way to get people totally lost about what they're writing, and this is a coercion from a coercion to a coercion. Regardless of whether type class inference will get confused, people will get confused.

view this post on Zulip Reid Barton (Aug 13 2020 at 18:52):

I'm not trying to argue for the coercion, I just don't see why it would be particularly problematic (I also don't find this confusing because coercing a set to a subtype is super common, but YMMV).

view this post on Zulip Eric Wieser (Aug 13 2020 at 19:09):

Would these be sensible as has_lift instead of has_coe?

view this post on Zulip Utensil Song (Aug 14 2020 at 12:15):

Eric Wieser said:

since the type gets smaller

Does that then mean that has_coe ↥A ↥(A ∪ B) would _not_ be sensible / safe?

Does it even work?

view this post on Zulip Utensil Song (Aug 14 2020 at 13:19):

{X Y : Type*} {A B : set X} (f : A → Y) (g: B → Y) (h : ∀ x : A ∩ B, f x = g x) is playing an even more dangerous game.

view this post on Zulip Utensil Song (Aug 14 2020 at 13:30):

For an x ∈ A ∩ B, its type should be X. Writing x : A ∩ B is nowhere near what you meant to express.

Same for f and g, they are not mapping the members of A and B to Y, so they are also not expressing functions that have a domain.

view this post on Zulip Eric Wieser (Aug 14 2020 at 14:37):

Writing x : A ∩ B is nowhere near what you meant to express.

It's not far off - it's identical to {x : {x' : X // x' ∈ A ∩ B}) which is not that different from saying(x : X) (h : x ∈ A ∩ B)

view this post on Zulip Eric Wieser (Aug 14 2020 at 14:39):

they are not mapping the members of A and B to Y

I'm confused by your statement - that's exactly what they're doing - they're partial functions over X that only accept members of A and B.

view this post on Zulip Utensil Song (Aug 14 2020 at 15:40):

Oh, I didn't recognize them as identical until I saw

/-- Coercion from a set to the corresponding subtype. -/
instance {α : Type*} : has_coe_to_sort (set α) := ⟨_, λ s, {x // x  s}

Last updated: May 14 2021 at 05:20 UTC