SCALA '21: "Implementing Path-Dependent ..."
Implementing Path-Dependent GADT Reasoning for Scala 3
Yichen Xu, Aleksander Boruch-Gruszecki, and Lionel Parreaux
(Beijing University of Posts and Telecommunications, China; EPFL, Switzerland; Hong Kong University of Science and Technology, China)
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.
@InProceedings{SCALA21p22,
author = {Yichen Xu and Aleksander Boruch-Gruszecki and Lionel Parreaux},
title = {Implementing Path-Dependent GADT Reasoning for Scala 3},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {22--32},
doi = {10.1145/3486610.3486892},
year = {2021},
}
Publisher's Version
SCALA '21: "Safer Exceptions for Scala ..."
Safer Exceptions for Scala
Martin Odersky, Aleksander Boruch-Gruszecki, Jonathan Immanuel Brachthäuser, Edward Lee, and Ondřej Lhoták
(EPFL, Switzerland; University of Waterloo, Canada)
We describe a scheme for reflecting exceptions as capabilities in the Scala type system that keeps notational overhead to a minimum and avoids well-known problems with Java's checked exceptions framework. The scheme makes exceptions safer but not fully safe since the capability for throwing an exception may still yet escape its enclosing try block. To address this limitation, we also propose a type system which prevents capabilities from escaping.
@InProceedings{SCALA21p1,
author = {Martin Odersky and Aleksander Boruch-Gruszecki and Jonathan Immanuel Brachthäuser and Edward Lee and Ondřej Lhoták},
title = {Safer Exceptions for Scala},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {1--11},
doi = {10.1145/3486610.3486893},
year = {2021},
}
Publisher's Version
SCALA '21: "Safer Exceptions for Scala ..."
Safer Exceptions for Scala
Martin Odersky, Aleksander Boruch-Gruszecki, Jonathan Immanuel Brachthäuser, Edward Lee, and Ondřej Lhoták
(EPFL, Switzerland; University of Waterloo, Canada)
We describe a scheme for reflecting exceptions as capabilities in the Scala type system that keeps notational overhead to a minimum and avoids well-known problems with Java's checked exceptions framework. The scheme makes exceptions safer but not fully safe since the capability for throwing an exception may still yet escape its enclosing try block. To address this limitation, we also propose a type system which prevents capabilities from escaping.
@InProceedings{SCALA21p1,
author = {Martin Odersky and Aleksander Boruch-Gruszecki and Jonathan Immanuel Brachthäuser and Edward Lee and Ondřej Lhoták},
title = {Safer Exceptions for Scala},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {1--11},
doi = {10.1145/3486610.3486893},
year = {2021},
}
Publisher's Version
SCALA '21: "Safer Exceptions for Scala ..."
Safer Exceptions for Scala
Martin Odersky, Aleksander Boruch-Gruszecki, Jonathan Immanuel Brachthäuser, Edward Lee, and Ondřej Lhoták
(EPFL, Switzerland; University of Waterloo, Canada)
We describe a scheme for reflecting exceptions as capabilities in the Scala type system that keeps notational overhead to a minimum and avoids well-known problems with Java's checked exceptions framework. The scheme makes exceptions safer but not fully safe since the capability for throwing an exception may still yet escape its enclosing try block. To address this limitation, we also propose a type system which prevents capabilities from escaping.
@InProceedings{SCALA21p1,
author = {Martin Odersky and Aleksander Boruch-Gruszecki and Jonathan Immanuel Brachthäuser and Edward Lee and Ondřej Lhoták},
title = {Safer Exceptions for Scala},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {1--11},
doi = {10.1145/3486610.3486893},
year = {2021},
}
Publisher's Version
SCALA '21: "Safer Exceptions for Scala ..."
Safer Exceptions for Scala
Martin Odersky, Aleksander Boruch-Gruszecki, Jonathan Immanuel Brachthäuser, Edward Lee, and Ondřej Lhoták
(EPFL, Switzerland; University of Waterloo, Canada)
We describe a scheme for reflecting exceptions as capabilities in the Scala type system that keeps notational overhead to a minimum and avoids well-known problems with Java's checked exceptions framework. The scheme makes exceptions safer but not fully safe since the capability for throwing an exception may still yet escape its enclosing try block. To address this limitation, we also propose a type system which prevents capabilities from escaping.
@InProceedings{SCALA21p1,
author = {Martin Odersky and Aleksander Boruch-Gruszecki and Jonathan Immanuel Brachthäuser and Edward Lee and Ondřej Lhoták},
title = {Safer Exceptions for Scala},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {1--11},
doi = {10.1145/3486610.3486893},
year = {2021},
}
Publisher's Version
SCALA '21: "Safe Object Initialization, ..."
Safe Object Initialization, Abstractly
Fengyun Liu, Ondřej Lhoták, Enze Xing, and Nguyen Cao Pham
(Oracle Labs, Switzerland; University of Waterloo, Canada)
Objects under initialization are fragile: some of their fields are not yet initialized. Consequently, accessing those uninitialized fields directly or indirectly may result in program crashes or abnormal behaviors at runtime.
A newly created object goes through several states during its initialization, beginning with all fields being empty until all of them are filled. However, ensuring initialization safety statically, without manual annotation of initialization states in the source code, is a challenge, due to aliasing, virtual method calls and typestate polymorphism.
In this work, we introduce a novel analysis based on abstract interpreters to ensure initialization safety. Compared to the previous approaches, our analysis is simpler and easier to extend, and it does not require any user annotations. The analysis is inter-procedural, context-sensitive and flow-insensitive, yet it has good performance thanks to local reasoning and heap monotonicity.
@InProceedings{SCALA21p33,
author = {Fengyun Liu and Ondřej Lhoták and Enze Xing and Nguyen Cao Pham},
title = {Safe Object Initialization, Abstractly},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {33--43},
doi = {10.1145/3486610.3486895},
year = {2021},
}
Publisher's Version
SCALA '21: "Safe Object Initialization, ..."
Safe Object Initialization, Abstractly
Fengyun Liu, Ondřej Lhoták, Enze Xing, and Nguyen Cao Pham
(Oracle Labs, Switzerland; University of Waterloo, Canada)
Objects under initialization are fragile: some of their fields are not yet initialized. Consequently, accessing those uninitialized fields directly or indirectly may result in program crashes or abnormal behaviors at runtime.
A newly created object goes through several states during its initialization, beginning with all fields being empty until all of them are filled. However, ensuring initialization safety statically, without manual annotation of initialization states in the source code, is a challenge, due to aliasing, virtual method calls and typestate polymorphism.
In this work, we introduce a novel analysis based on abstract interpreters to ensure initialization safety. Compared to the previous approaches, our analysis is simpler and easier to extend, and it does not require any user annotations. The analysis is inter-procedural, context-sensitive and flow-insensitive, yet it has good performance thanks to local reasoning and heap monotonicity.
@InProceedings{SCALA21p33,
author = {Fengyun Liu and Ondřej Lhoták and Enze Xing and Nguyen Cao Pham},
title = {Safe Object Initialization, Abstractly},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {33--43},
doi = {10.1145/3486610.3486895},
year = {2021},
}
Publisher's Version
SCALA '21: "Pathless Scala: A Calculus ..."
Pathless Scala: A Calculus for the Rest of Scala
Guillaume Martres
(EPFL, Switzerland)
Recent work on the DOT calculus successfully put core aspects of Scala on a sound foundation, but subtyping in DOT is structural and therefore not easily amenable to studying the parts of Scala that are deeply tied to its nominal subtyping system. On the other hand, the Featherweight Java calculus has proven to be a great basis for studying many aspects of Java and Java-like languages. Continuing this tradition, we present Pathless Scala: an extension of Featherweight Generic Java that closely models multiple inheritance and intersection types as they exist in the Scala language today. We define the semantics of Pathless Scala by erasing it to a simpler calculus in a way that closely models how Scala is compiled to Java bytecode in practice. More than a one-off, we believe that this calculus could be extended to describe many more features of Scala, although reconciling it with DOT remains an open problem.
@InProceedings{SCALA21p12,
author = {Guillaume Martres},
title = {Pathless Scala: A Calculus for the Rest of Scala},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {12--21},
doi = {10.1145/3486610.3486894},
year = {2021},
}
Publisher's Version
SCALA '21: "Safer Exceptions for Scala ..."
Safer Exceptions for Scala
Martin Odersky, Aleksander Boruch-Gruszecki, Jonathan Immanuel Brachthäuser, Edward Lee, and Ondřej Lhoták
(EPFL, Switzerland; University of Waterloo, Canada)
We describe a scheme for reflecting exceptions as capabilities in the Scala type system that keeps notational overhead to a minimum and avoids well-known problems with Java's checked exceptions framework. The scheme makes exceptions safer but not fully safe since the capability for throwing an exception may still yet escape its enclosing try block. To address this limitation, we also propose a type system which prevents capabilities from escaping.
@InProceedings{SCALA21p1,
author = {Martin Odersky and Aleksander Boruch-Gruszecki and Jonathan Immanuel Brachthäuser and Edward Lee and Ondřej Lhoták},
title = {Safer Exceptions for Scala},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {1--11},
doi = {10.1145/3486610.3486893},
year = {2021},
}
Publisher's Version
SCALA '21: "Implementing Path-Dependent ..."
Implementing Path-Dependent GADT Reasoning for Scala 3
Yichen Xu, Aleksander Boruch-Gruszecki, and Lionel Parreaux
(Beijing University of Posts and Telecommunications, China; EPFL, Switzerland; Hong Kong University of Science and Technology, China)
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.
@InProceedings{SCALA21p22,
author = {Yichen Xu and Aleksander Boruch-Gruszecki and Lionel Parreaux},
title = {Implementing Path-Dependent GADT Reasoning for Scala 3},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {22--32},
doi = {10.1145/3486610.3486892},
year = {2021},
}
Publisher's Version
SCALA '21: "Safe Object Initialization, ..."
Safe Object Initialization, Abstractly
Fengyun Liu, Ondřej Lhoták, Enze Xing, and Nguyen Cao Pham
(Oracle Labs, Switzerland; University of Waterloo, Canada)
Objects under initialization are fragile: some of their fields are not yet initialized. Consequently, accessing those uninitialized fields directly or indirectly may result in program crashes or abnormal behaviors at runtime.
A newly created object goes through several states during its initialization, beginning with all fields being empty until all of them are filled. However, ensuring initialization safety statically, without manual annotation of initialization states in the source code, is a challenge, due to aliasing, virtual method calls and typestate polymorphism.
In this work, we introduce a novel analysis based on abstract interpreters to ensure initialization safety. Compared to the previous approaches, our analysis is simpler and easier to extend, and it does not require any user annotations. The analysis is inter-procedural, context-sensitive and flow-insensitive, yet it has good performance thanks to local reasoning and heap monotonicity.
@InProceedings{SCALA21p33,
author = {Fengyun Liu and Ondřej Lhoták and Enze Xing and Nguyen Cao Pham},
title = {Safe Object Initialization, Abstractly},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {33--43},
doi = {10.1145/3486610.3486895},
year = {2021},
}
Publisher's Version
SCALA '21: "Safe Object Initialization, ..."
Safe Object Initialization, Abstractly
Fengyun Liu, Ondřej Lhoták, Enze Xing, and Nguyen Cao Pham
(Oracle Labs, Switzerland; University of Waterloo, Canada)
Objects under initialization are fragile: some of their fields are not yet initialized. Consequently, accessing those uninitialized fields directly or indirectly may result in program crashes or abnormal behaviors at runtime.
A newly created object goes through several states during its initialization, beginning with all fields being empty until all of them are filled. However, ensuring initialization safety statically, without manual annotation of initialization states in the source code, is a challenge, due to aliasing, virtual method calls and typestate polymorphism.
In this work, we introduce a novel analysis based on abstract interpreters to ensure initialization safety. Compared to the previous approaches, our analysis is simpler and easier to extend, and it does not require any user annotations. The analysis is inter-procedural, context-sensitive and flow-insensitive, yet it has good performance thanks to local reasoning and heap monotonicity.
@InProceedings{SCALA21p33,
author = {Fengyun Liu and Ondřej Lhoták and Enze Xing and Nguyen Cao Pham},
title = {Safe Object Initialization, Abstractly},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {33--43},
doi = {10.1145/3486610.3486895},
year = {2021},
}
Publisher's Version
SCALA '21: "Implementing Path-Dependent ..."
Implementing Path-Dependent GADT Reasoning for Scala 3
Yichen Xu, Aleksander Boruch-Gruszecki, and Lionel Parreaux
(Beijing University of Posts and Telecommunications, China; EPFL, Switzerland; Hong Kong University of Science and Technology, China)
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.
@InProceedings{SCALA21p22,
author = {Yichen Xu and Aleksander Boruch-Gruszecki and Lionel Parreaux},
title = {Implementing Path-Dependent GADT Reasoning for Scala 3},
booktitle = {Proc.\ SCALA},
publisher = {ACM},
pages = {22--32},
doi = {10.1145/3486610.3486892},
year = {2021},
}
Publisher's Version