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.''
# Please note that Dependent ML (DML) is no longer under active development. As a language, it has already been fully incorporated into ATS. # Dependent ML (DML) is a conservative extension of the functional programming language ML. The type system of DML enriches that of ML with a restricted form of dependent types. This allows many interesting program properties such as memory safety and termination to be captured in the type system of DML and therefore be verified at compiler-time. # DML The current (undocumented) implementation of a DML type-checker can be found here, which is written in Objective Caml. The syntax of DML can be readily learned from the various examples included in the distribution given that one is already familiar with Standard ML. Also, termination checking is supported in this implementation. # de Caml is the Caml-light compiler extended with a front-end supporting DML style dependent types.
G'Caml is a variant of O'Caml compiler which extends ML parametric polymorphism to non-parametric one, called extensional polymorphism. Freed from the clear but simple parametricity, G'Caml provides many useful features which were impossible or very hard to achieve in O'Caml, such as overloading, type safe value marshalling, ML value printer, etc., Overloading Values of different types can be overloaded to one identifier, i.e. (+) and (+.) will be unified! Built-in ML value printer Gprint.print prints your ML value as if you were in toplevel. You no longer need to define trivial but boring printers by yourself. Type safe value input/output Value marshaling (serialization) is now type-safe. Types of types are now checked at input, so that ill-typed value input is rejected at run-time, instead of crashing the program.