Zulip Chat Archive

Stream: new members

Topic: Subtype covariance


Martin Dvořák (Feb 02 2022 at 19:43):

Does Lean have any feature for covariance with respect to subtypes? I have a type T and its subtype S. I can tag the definition of S with @[reducible] in case it matters. I have a term of type list S. Can I use it in a position of an argument of type list T please? I suspect it doesn't work like that with list but maybe, with some custom types, does it work? I want to use it for types depending on types.

Kyle Miller (Feb 02 2022 at 19:52):

The only way I know how to do this is to explicitly write l.map coe to coerce the elements of a list. (That is, you use the map functor to manage covariance yourself.)

(It might be interesting if there were an attribute (not implemented yet) that you could tag a function to be able to try to automatically construct a subtype version.)

Kyle Miller (Feb 02 2022 at 19:53):

Can you make an #mwe of the function to show what you want to do? There might be other solutions.

Martin Dvořák (Feb 02 2022 at 19:58):

Making an MWE for my use case will be a bit harder but I will try.

Yakov Pechersky (Feb 02 2022 at 19:59):

We do have lift instances for list, for going the other way, via tactics

Martin Dvořák (Feb 02 2022 at 19:59):

For input argument? The other way?!

Martin Dvořák (Feb 03 2022 at 10:09):

Yakov Pechersky said:

We do have lift instances for list, for going the other way, via tactics

Can you please explain?

Yakov Pechersky (Feb 03 2022 at 14:29):

First of all, we have a general docs#coe_subtype. I was referring to docs#lift_list

Martin Dvořák (Feb 04 2022 at 15:08):

Does has_lift come automatically whenever we create a subtype? And can we have has_lift for something that is not a subtype?


Last updated: Dec 20 2023 at 11:08 UTC