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

Georg Stefan Schmid, Olivier Blanvillain, Jad Hamza +1

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 progra…