This paper describes practical programming with types parameterized by numbers: e.g., an array type parameterized by the array's size or a modular group type Zn parameterized by the modulus. An attempt to add, for example, two integers of different moduli should result in a compile-time error with a clear error message. Number-parameterized types let the programmer capture more invariants through types and eliminate some run-time checks. Oleg shows several approaches towards encoding numbers into types and using those numbers to check list length, matching sizes for matrices or vectors. Oleg also points out connections to dependent types, phantom types, and shape-invariant programming.
1. What is a dependent type 1. ADT -- the simplest dependent-type 2. Singleton types 3. Branding: type proxies 2. Lightweight static capabilities 1. Abstract and Introduction 2. Formalization and proofs 3. Accompanying source code 3. The question of verification 4. Genuine Dependent-type systems This is a joint work with Chung-chieh Shan. We describe several approaches to lightweight dependent-type programming, letting us gain experience with dependent types on existing programming language systems All these lightweight approaches rely on type-level proxies for values, so we can statically express properties (e.g., equality, inequality) of the values that are not generally known until the run time. ``This much is clear: many programmers are already finding practical uses for the approximants to dependent types which mainstream functional languages (especially Haskell) admit, by hook or by crook.''