#
Simulating Dependent Types with Guarded Algebraic Datatypes

by Jim Apple and Wes Weimer

This page holds all materials for the draft paper Simulating Dependent
Types with Guarded Algebraic Datatypes.

## Abstract:

Dependent type systems, in which types can depend on values, admit
detailed specifications of function behavior and data
invariants. Programming languages based on System F do not have
dependent types, and are therefore more limited in what structure or
function invariants can be encoded in the type system.

In this paper, we show how guarded algebraic datatypes can simulate
dependent types. We formalize additions to a
guarded-datatypes-enhanced System F that allow types to depend on
values and discuss the programming style that results, which is
similar to theorem proving. Our technique can be applied to multiple
existing programming languages, including Haskell and C#. We also
introduce an idiom for eliminating any execution cost from programming
with simulated dependent types. We have developed a tool to
automatically produce the boilerplate necessary for the simulation,
and we have used it to enforce data structure invariants and to allow
elision of run-time bounds checks.

## Files:

- The implementation:
- Some examples:

This document last modified Monday, 11-Aug-2008 14:58:25 EDT.