Implementing Path-Dependent GADT Reasoning for Scala 3
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 OctDisplayed time zone: Central Time (US & Canada) change
10:50 - 12:10
|Implementing Path-Dependent GADT Reasoning for Scala 3|
Yichen Xu Beijing University of Posts and Telecommunications, Aleksander Boruch-Gruszecki EPFL, Lionel Parreaux Hong Kong University of Science and TechnologyDOI
|Safe Object Initialization, Abstractly|
Fengyun Liu Oracle Labs, Ondřej Lhoták University of Waterloo, Enze Xing University of Waterloo, Nguyen Cao Pham University of WaterlooDOI