Implementing path-dependent GADT reasoning for Scala 3

Yichen Xu; Aleksander Boruch-Gruszecki; Lionel Parreaux

doi:10.1145/3486610.3486892

Implementing path-dependent GADT reasoning for Scala 3

Yichen Xu, Aleksander Boruch-Gruszecki, Lionel Parreaux

Department of Computer Science and Engineering

Research output: Chapter in Book/Conference Proceeding/Report › Conference Paper published in a book › peer-review

1 Citation (Scopus)

Abstract

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.

Original language	English
Title of host publication	SCALA 2021 - Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, co-located with SPLASH 2021
Editors	Julien Richard-Foy, Sebastien Doeraene
Publisher	Association for Computing Machinery, Inc
Pages	22-32
Number of pages	11
ISBN (Electronic)	9781450391139
DOIs	https://doi.org/10.1145/3486610.3486892
Publication status	Published - 17 Oct 2021
Event	12th ACM SIGPLAN International Symposium on Scala, SCALA 2021, co-located with SPLASH 2021 - Virtual, Online, United States Duration: 17 Oct 2021 → …

Publication series

Name	SCALA 2021 - Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, co-located with SPLASH 2021

Conference

Conference	12th ACM SIGPLAN International Symposium on Scala, SCALA 2021, co-located with SPLASH 2021
Country/Territory	United States
City	Virtual, Online
Period	17/10/21 → …

Bibliographical note

Publisher Copyright:
© 2021 ACM.

Keywords

Generalized algebraic data types
Path-dependent types
Scala
Singleton types
Type members

Access to Document

10.1145/3486610.3486892

Cite this

Xu, Y., Boruch-Gruszecki, A., & Parreaux, L. (2021). Implementing path-dependent GADT reasoning for Scala 3. In J. Richard-Foy, & S. Doeraene (Eds.), SCALA 2021 - Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, co-located with SPLASH 2021 (pp. 22-32). (SCALA 2021 - Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, co-located with SPLASH 2021). Association for Computing Machinery, Inc. https://doi.org/10.1145/3486610.3486892

Xu, Yichen ; Boruch-Gruszecki, Aleksander ; Parreaux, Lionel. / Implementing path-dependent GADT reasoning for Scala 3. SCALA 2021 - Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, co-located with SPLASH 2021. editor / Julien Richard-Foy ; Sebastien Doeraene. Association for Computing Machinery, Inc, 2021. pp. 22-32 (SCALA 2021 - Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, co-located with SPLASH 2021).

@inproceedings{a2af744364e94b7eb183b31541ee169b,

title = "Implementing path-dependent GADT reasoning for Scala 3",

abstract = "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.",

keywords = "Generalized algebraic data types, Path-dependent types, Scala, Singleton types, Type members",

author = "Yichen Xu and Aleksander Boruch-Gruszecki and Lionel Parreaux",

note = "Publisher Copyright: {\textcopyright} 2021 ACM.; 12th ACM SIGPLAN International Symposium on Scala, SCALA 2021, co-located with SPLASH 2021 ; Conference date: 17-10-2021",

year = "2021",

month = oct,

day = "17",

doi = "10.1145/3486610.3486892",

language = "English",

series = "SCALA 2021 - Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, co-located with SPLASH 2021",

publisher = "Association for Computing Machinery, Inc",

pages = "22--32",

editor = "Julien Richard-Foy and Sebastien Doeraene",

booktitle = "SCALA 2021 - Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, co-located with SPLASH 2021",

}

Xu, Y, Boruch-Gruszecki, A & Parreaux, L 2021, Implementing path-dependent GADT reasoning for Scala 3. in J Richard-Foy & S Doeraene (eds), SCALA 2021 - Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, co-located with SPLASH 2021. SCALA 2021 - Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, co-located with SPLASH 2021, Association for Computing Machinery, Inc, pp. 22-32, 12th ACM SIGPLAN International Symposium on Scala, SCALA 2021, co-located with SPLASH 2021, Virtual, Online, United States, 17/10/21. https://doi.org/10.1145/3486610.3486892

Implementing path-dependent GADT reasoning for Scala 3. / Xu, Yichen; Boruch-Gruszecki, Aleksander; Parreaux, Lionel.
SCALA 2021 - Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, co-located with SPLASH 2021. ed. / Julien Richard-Foy; Sebastien Doeraene. Association for Computing Machinery, Inc, 2021. p. 22-32 (SCALA 2021 - Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, co-located with SPLASH 2021).

Research output: Chapter in Book/Conference Proceeding/Report › Conference Paper published in a book › peer-review

TY - GEN

T1 - Implementing path-dependent GADT reasoning for Scala 3

AU - Xu, Yichen

AU - Boruch-Gruszecki, Aleksander

AU - Parreaux, Lionel

PY - 2021/10/17

Y1 - 2021/10/17

N2 - 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.

AB - 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.

KW - Generalized algebraic data types

KW - Path-dependent types

KW - Scala

KW - Singleton types

KW - Type members

UR - https://openalex.org/W3205228179

UR - https://www.scopus.com/pages/publications/85121109155

U2 - 10.1145/3486610.3486892

DO - 10.1145/3486610.3486892

M3 - Conference Paper published in a book

T3 - SCALA 2021 - Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, co-located with SPLASH 2021

SP - 22

EP - 32

BT - SCALA 2021 - Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, co-located with SPLASH 2021

A2 - Richard-Foy, Julien

A2 - Doeraene, Sebastien

PB - Association for Computing Machinery, Inc

T2 - 12th ACM SIGPLAN International Symposium on Scala, SCALA 2021, co-located with SPLASH 2021

Y2 - 17 October 2021

ER -

Xu Y, Boruch-Gruszecki A, Parreaux L. Implementing path-dependent GADT reasoning for Scala 3. In Richard-Foy J, Doeraene S, editors, SCALA 2021 - Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, co-located with SPLASH 2021. Association for Computing Machinery, Inc. 2021. p. 22-32. (SCALA 2021 - Proceedings of the 12th ACM SIGPLAN International Symposium on Scala, co-located with SPLASH 2021). doi: 10.1145/3486610.3486892

Implementing path-dependent GADT reasoning for Scala 3

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this