Zulip Chat Archive

Stream: new members

Topic: subtype coercion to supertype


view this post on Zulip Kevin Kappelmann (Jun 11 2019 at 11:46):

I was wondering if I use subtypes (and coercions to their supertype) correctly. For example, let's define a subtype of lists of length, say, at most 5:

def short_list (α : Type*) := {l : list α // l.length  5}

Now, given some sl : short_list α, I naturally would like to re-use functions from list. For example:

variables (α : Type*) (sl : short_list α)
/- What I would like to have -/
#check list.length sl -- error - expected list but got short_list
/- What also does not work -/
#check list.length (sl : list α) -- error since no coercion to list is known
/- What works but is not what I want -/
#check list.length sl.val

So what I ended up doing is this:

instance short_list_to_list : has_coe (short_list α) (list α) := ⟨λ sl, sl.val

@[simp, elim_cast]
lemma coe_short_list (sl : short_list α) : (sl : list α) = sl.val :=
by refl

/- Works -/
#check list.length (sl : list α)
/- Does not work -/
#check list.length sl

Is this the best I can do? Is it the right thing to do? If so, shouldn't these kind of coercions be created automatically?

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 12:55):

I guess that short_list alpha is a wrapper for subtype, so even if there was a coercion from subtype it wouldn't trigger for short_lists.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 12:58):

import data.subtype

def short_list (α : Type*) := {l : list α // l.length  5}

instance subtype_coe_thing (α : Type*) (P : α  Prop) :
has_coe {a : α // P a} α := ⟨λ x, x.val

variables (α : Type*) (sl : short_list α)
variable (sl' : {l : list α // l.length  5})

-- #check list.length (sl : list α) -- fails
#check list.length (sl' : list α) -- works

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 13:00):

--instance short_list_to_list : has_coe (short_list α) (list α) := by apply_instance -- fails

instance short_list_to_list : has_coe (short_list α) (list α) :=
  by unfold short_list; apply_instance -- works

I could imagine that sometimes people make these wrapper definitions precisely to switch _off_ some automatic coercion!

view this post on Zulip Kevin Kappelmann (Jun 11 2019 at 13:23):

Oh great, that's exactly what I was looking for - thanks a lot Kevin :)

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 13:24):

I'm not sure it is :-(

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 13:24):

I still had to coerce to list alpha.

view this post on Zulip Kevin Kappelmann (Jun 11 2019 at 13:30):

Hah, yeah - let me rephrase: the subtype_coe_thing part was exactly what I was having in my mind, that is a general coercion from subtypes to supertypes. The explicit coercion to list is still not "perfect".

view this post on Zulip Kevin Kappelmann (Jun 11 2019 at 13:32):

Moreover, I'd be very interested why that kind of automatic coercion is not enabled/built in. On a similar note, one cannot cast datatypes if the carrier type has a coercion. For example:

#check (([1,2,3] : list ) : list ) -- fails

variables {β γ : Type} [has_coe β γ]
instance option_to_option : has_coe (list β) (list  γ) := ⟨λ l, l.map (λ b, (b : γ))

#check (([1,2,3] : list ) : list ) -- works

Last updated: May 06 2021 at 20:13 UTC