Subtype covariance

Stream: new members

[Martin Dvořák]

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]

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]

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

[Martin Dvořák]

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

[Yakov Pechersky]

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

[Martin Dvořák]

For input argument? The other way?!

[Martin Dvořák]

Yakov Pechersky said:

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

Can you please explain?

[Yakov Pechersky]

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

[Martin Dvořák]

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