Towards improved GADT reasoning in Scala

None, None; None, None; None, None

Towards improved GADT reasoning in Scala

Conference Paper (2019)

Author(s)

Lionel Parreaux (École Polytechnique Fédérale de Lausanne)

Aleksander Boruch-Gruszecki (École Polytechnique Fédérale de Lausanne)

Paolo G. Giarrusso (TU Delft - Electrical Engineering, Mathematics and Computer Science)

Research Group

Programming Languages

Scala DOT Generalized algebraic data types

DOI related publication

https://doi.org/10.1145/3337932.3338813 Final published version

To reference this document use

https://resolver.tudelft.nl/uuid:7f958c14-af9a-4103-a9cf-611024f3bd36

More Info

expand_more

Publication Year

2019

Language

English

Research Group

Programming Languages

Pages (from-to)

12-16

ISBN (electronic)

9781450368247

Event

10th ACM SIGPLAN International Symposium on Scala, Scala 2019, co-located with the European Conference on Object-Oriented Programming, ECOOP 2019, London, United Kingdom

Downloads counter

125

Abstract

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.