Practical Datatype Specializations with Phantom Types and Recursion Schemes
Loading...
Date
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Description
Datatype specialization is a form of subtyping that captures program invariants on data structures that are expressed using the convenient and intuitive datatype notation. Of particular interest are structural invariants such as well-formedness. We investigate the use of phantom types for describing datatype specializations. We show that it is possible to express statically-checked specializations within the type system of Standard ML. We also show that this can be done in a way that does not lose useful programming facilities such as pattern matching in case expressions.
25 pages. Appeared in the Proc. of the 2005 ACM SIGPLAN Workshop on ML
25 pages. Appeared in the Proc. of the 2005 ACM SIGPLAN Workshop on ML