Towards Improved GADT Reasoning in Scala
Generalized algebraic data types (GADT) have been notoriously difficult to implement correctly in Scala. Both major Scala compilers, Scalac and Dotty, are currently known to have type soundness holes related to them. In particular, covariant GADTs have exposed paradoxes due to Scala's inheritance model. We informally explore foundations for GADTs within Scala's core type system, to guide a principled understanding and implementation of GADTs in Scala.
Cite this item
Parreaux, L., Boruch-Gruszecki, A., & Giarrusso, P. G. (2019). Towards Improved GADT Reasoning in Scala. Scala′19: Proceedings of the 10Th Acm Sigplan International Symposium on Scala, 12–16. https://doi.org/10.1145/3337932.3338813
Click Copy to copy the citation, or select the text manually.
3337932.3338813.pdf
Publisher's Version
Published version
openaccess
CC BY-SA
463.97 KB
Adobe PDF
b8ee9af3e4e63313f70a972986498925