English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Type-level programming is an increasingly popular way to obtain additionaltype safety. Unfortunately, it remains a second-class citizen in the majorityof industrially-used programming languages. We propose a new dependently-typedsystem with subtyping and singleton types whose goal is to enable type-levelprogramming in an accessible style. At the heart of our system lies anon-deterministic choice operator. We argue that embracing non-determinism iscrucial for bringing dependent types to a broader audience of programmers,since real-world programs will inevitably interact with imprecisely-typed, oreven impure code. Furthermore, we show that singleton types combined with thechoice operator can serve as a replacement for many type functions of interestin practice. We establish the soundness of our approach using the Coq proofassistant. Our soundness approach models non-determinism using additionalfunction arguments to represent choices. We represent type-level computationusing singleton types and existential types that quantify over choicearguments. To demonstrate the practicality of our type system, we present animplementation as a modification of the Scala compiler. We provide a case studyin which we develop a strongly-typed wrapper for Spark datasets.

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