WebPie: A Tiny Slice of Dependent Typing
Christophe Scholliers
TL;DR
WebPie provides a compact, implementable setting for studying dependent types by starting from a minimal language (WebLF) and extending it with inductive types, case analysis, and guarded recursion. It frames dependent types through the Curry–Howard correspondence and demonstrates practical encodings of logic and arithmetic (e.g., first-order logic and natural numbers) within WebLF, then extends to WebPie to support inductive definitions, case splitting, and terminating recursion. The paper formalizes WebLF’s syntax, typing, substitution, and normalization, and discusses a JavaScript implementation using algebraic data types, offering a hands-on path from theory to implementation. Overall, it aims to bridge theory and practice by enabling researchers and students to experiment with core dependent-type constructs in a small, approachable language.
Abstract
Dependently typed programming languages have become increasingly relevant in recent years. They have been adopted in industrial strength programming languages and have been extremely successful as the basis for theorem provers. There are however, very few entry level introductions to the theory of language constructs for dependently typed languages, and even less sources on didactical implementations. In this paper, we present a small dependently typed programming language called WebPie. The main features of the language are inductive types, recursion and case matching. While none of these features are new, we believe this article can provide a step forward towards the understanding and systematic construction of dependently typed languages for researchers new to dependent types.