A Generic Algorithm for Checking Exhaustivity of Pattern Matching (Short Paper)
Algebraic data types and pattern matching are key features of functional programming languages. Exhaustivity checking of pattern matching is a safety belt that defends against unmatched exceptions at runtime and boosts type safety. However, the presence of language features like inheritance, typecase, traits, GADTs, path-dependent types and union types makes the checking difficult and the algorithm complex.
In this paper we propose a generic algorithm that decouples the checking algorithm from specific type theories. The decoupling makes the algorithm simple and enables easy customization for specific type systems.
I’m a PhD student at EPFL. My interested areas are type systems, effect systems, programming languages, and various logics.
Sun 30 OctDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:10
|Implementing Higher-Kinded Types in Dotty|
Martin Odersky EPFL, Switzerland, Guillaume Martres EPFL, Switzerland, Dmitry Petrashko EPFL, SwitzerlandDOI Pre-print Media Attached
Sébastien Doeraene EPFL, Switzerland, Tobias Schlatter EPFL, Switzerland, Nicolas Stucki EPFL, SwitzerlandDOI Pre-print
|A Generic Algorithm for Checking Exhaustivity of Pattern Matching (Short Paper)|
Fengyun Liu EPFL, SwitzerlandDOI Media Attached
|Scaps: Type-Directed API Search for Scala|
Lukas Wegmann 1plusX, Switzerland, Farhad Mehta University of Applied Sciences Rapperswil, Switzerland, Peter Sommerlad University of Applied Sciences Rapperswil, Switzerland, Mirko Stocker University of Applied Sciences Rapperswil, SwitzerlandDOI File Attached