SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Sun 17 Oct 2021 10:50 - 11:10 at Zurich E - Session 2 Chair(s): Sébastien Doeraene

Generalized Algebraic Data Types (GADT) are a popular programming language feature allowing advanced type-level properties to be encoded in the data types of a program. While Scala does not have direct support for them, GADT definitions can be encoded through Scala class hierarchies. Moreover, the Scala 3 compiler recently augmented its pattern matching capabilities to reason about such class hierarchies, making GADT-based programming practical in Scala. However, the current implementation can only reason about type parameters, but Scala’s type system also features singleton types and abstract type members (collectively known as path-dependent types), about which GADT-style reasoning is also useful and important. In this paper, we show how we extended the existing constraint-based GADT reasoning of the Scala 3 compiler to also consider path-dependent types, making Scala’s support for GADT programming more complete and bringing Scala closer to its formal foundations.

Sun 17 Oct

Displayed time zone: Central Time (US & Canada) change

10:50 - 12:10
Session 2Scala at Zurich E
Chair(s): Sébastien Doeraene EPFL, Switzerland
10:50
20m
Full-paper
Implementing Path-Dependent GADT Reasoning for Scala 3
Scala
Yichen Xu Beijing University of Posts and Telecommunications, Aleksander Boruch-Gruszecki EPFL, Lionel Parreaux Hong Kong University of Science and Technology
DOI
11:10
20m
Full-paper
Safe Object Initialization, Abstractly
Scala
Fengyun Liu Oracle Labs, Ondřej Lhoták University of Waterloo, Enze Xing University of Waterloo, Nguyen Cao Pham University of Waterloo
DOI