Paper: Subtyping Recursive Types modulo Associative Commutative Products
We would like to announce the availability of the following manuscript:
Subtyping Recursive Types modulo Associative Commutative Products
We study subtyping of recursive types in the presence of associative and
commutative products---that is, subtyping modulo a restricted form of type
isomorphisms. We show that this relation, which we claim is useful in
practice, is a composition of the usual subtyping relation with the recently
proposed notion of equality up to associativity and commutativity of products,
and we propose an efficient decision algorithm for it. We also provide an
automatic way of constructing coercions between related types.
The document is available at
Comments are welcome.
Roberto Di Cosmo