Practical Datatype Specializations

  • mlwrk05.pdf (with Riccardo Pucella; Appeared at ML Workshop '05; 20050929-MLWRK05.pdf)

    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.

    Supporting materials

    • dataspec.tgz (dataspec tool; version 0.1)

      A tool to mechanically generate an implementation of specializations from a concise datatype/withspec declaration.

      Compatible with SML/NJ 110.0.7 and MLton 20041109.

    • Examples
      • fmla.tgz (Code from the paper.)

        Specializations of a Boolean formula datatype are used to statically verify that a toDNF function yields a formula in Disjunctive Normal Form.

      • rb-tree.tgz

        Specializations of a Red-Black Tree data-structure are used to statically verify that no red node has a red child after inserting a new element.

      • lambda.tgz

        Typed AST for deBruijn-based lambda calculus.

The documents contained in these directories are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.