|ML 2007||START Conference Manager|
In this paper, we discuss an approach to type-indexed values based on the value-dependent encoding approach. We extend upon previous work in several ways. We present a technique that allows an existing value-dependent encoding to be extended with new values. We show how to encode type-indexed values over essentially all the ML types, including arbitrary mutually recursive datatypes. We also show how to compute fixed points over arbitrary products.
Our techniques have been implemented in Standard ML, do not compromise abstraction, and require only a fixed number of combinators.
|START Conference Manager (V2.54.4)|