2020/11/15 by Georg Stefan Schmid, Schmid, Georg Stefan, Olivier Blanvillain +5
Chemistry · Computer Science · #Chemical synthesis and alkaloids #D.3.1 #D.3.3 #FOS: Computer and information sciences #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2011.07653
openalex publication_date 2020/11/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Type-level programming is an increasingly popular way to obtain additional type safety. Unfortunately, it remains a second-class citizen in the majority of industrially-used programming languages. We propose a new dependently-typed system with subtyping and singleton types whose goal is to enable type-level programming in an accessible style. At the heart of our system lies a non-deterministic choice operator. We argue that embracing non-determinism is crucial for bringing dependent types to a broader audience of programmers, since real-world programs will inevitably interact with imprecisely-typed, or even impure code. Furthermore, we show that singleton types combined with the choice operator can serve as a replacement for many type functions of interest in practice. We establish the soundness of our approach using the Coq proof assistant. Our soundness approach models non-determinism using additional function arguments to represent choices. We represent type-level computation using singleton types and existential types that quantify over choice arguments. To demonstrate the practicality of our type system, we present an implementation as a modification of the Scala compiler. We provide a case study in which we develop a strongly-typed wrapper for Spark datasets.