Coming to Terms with Your Choices: An Existential Take on Dependent Types

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