Name
Abstract | ||
|---|---|---|
While generalized algebraic datatypes (GADTs) are now considered well-understood, adding them to a language with a notion of subtyping comes with a few surprises. What does it mean for a GADT parameter to be covariant? The answer turns out to be quite subtle. It involves fine-grained properties of the subtyping relation that raise interesting design questions. We allow variance annotations in GADT definitions, study their soundness, and present a sound and complete algorithm to check them. Our work may be applied to real-world ML-like languages with explicit subtyping such as OCaml, or to languages with general subtyping constraints. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-37036-6_30 | ESOP'13 Proceedings of the 22nd European conference on Programming Languages and Systems |
Keywords | DocType | Volume |
subtyping relation,general subtyping constraint,generalized algebraic datatypes,ml-like language,interesting design question,complete algorithm,gadt definition,variance annotation,gadt parameter,fine-grained property | Conference | abs/1210.5935 |
ISSN | Citations | PageRank |
22nd European Symposium on Programming (ESOP), Rome : Italy (2013) | 1 | 0.39 |
References | Authors | |
3 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gabriel Scherer | 1 | 13 | 4.82 |
| Didier Rémy | 2 | 682 | 49.82 |