Coming to Terms with Your Choices: An Existential Take on Dependent Types
Georg Stefan Schmid (EPFL), Olivier Blanvillain (EPFL), Jad Hamza, (EPFL), Viktor Kun\v{c}ak (EPFL)

TL;DR
This paper introduces a dependently-typed system with subtyping and singleton types, incorporating non-determinism to make type-level programming more accessible and practical for real-world programming languages.
Contribution
It proposes a novel dependently-typed system with non-deterministic choice, singleton types, and subtyping, and demonstrates its soundness and practical implementation.
Findings
Soundness established via Coq proof assistant.
Practical implementation as a Scala compiler modification.
Case study on strongly-typed Spark dataset wrapper.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Chemical synthesis and alkaloids
