Practical Datatype Specializations with Phantom Types and Recursion Schemes
Programming Languages
2007-05-23 v1
Abstract
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.
Cite
@article{arxiv.cs/0510074,
title = {Practical Datatype Specializations with Phantom Types and Recursion Schemes},
author = {Matthew Fluet and Riccardo Pucella},
journal= {arXiv preprint arXiv:cs/0510074},
year = {2007}
}
Comments
25 pages. Appeared in the Proc. of the 2005 ACM SIGPLAN Workshop on ML