@inproceedings{MJS20_Zero-Cost-Constructor-Subtyping,
  author = {Marmaduke, Andrew and Jenkins, Christopher and Stump, Aaron},
  title = {Zero-Cost Constructor Subtyping},
  year = 2020,
  isbn = 9781450389631,
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3462172.3462194},
  doi = {10.1145/3462172.3462194},
  abstract = { Constructor subtyping is a form of subtyping where two inductive types can be related as long as the inductive signature of one is a subsignature of the other. To be a subsignature requires every constructor of the smaller datatype be present in the larger datatype (modulo subtyping of the constructors’ types). In this paper, we describe a method for impredicatively encoding datatype signatures in Cedille (a dependently typed programming language) that supports highly flexible constructor subtyping, with the subtyping relation given by a derived notion of type inclusion witnessed by a heterogeneously typed identity function. Specifically, the conditions under which constructor subtyping is possible between datatypes are fully independent of the order in which constructors are listed in their declarations. After examining some extended case studies, we formulate generically a sufficient condition for constructor subtyping in Cedille using our technique.},
  booktitle = {IFL 2020: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages},
  pages = {93–103},
  numpages = 11,
  keywords = {generic programming, impredicative encodings, Cedille, constructor subtyping},
  location = {Canterbury, United Kingdom},
  series = {IFL 2020},
}