Practical Datatype Specializations with Phantom Types and Recursion Schemes
<|reference_start|>Practical Datatype Specializations with Phantom Types and Recursion Schemes: 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.<|reference_end|>
@article{fluet2005practical,
    title={Practical Datatype Specializations with Phantom Types and Recursion
  Schemes},
    author={Matthew Fluet, Riccardo Pucella},
    journal={arXiv preprint arXiv:cs/0510074},
    year={2005},
    archivePrefix={arXiv},
    eprint={cs/0510074},
    primaryClass={cs.PL}
}