Polymorphism selectively and safely weakens a programming language’s type system when the difference between types isn’t important. Extensible Markup Language (XML) is a programming language with one operation: conformance to a schema, or document type definition (DTD). XML can be made polymorphic by assigning the string or binary data type to the portions of an XML document irrelevant to conformance. However, when XML is embedded in a programming language with a type system more advanced than XML’s, simple approaches to polymorphism are inadequate, particularly with respect to maintaining type safety.
Extensions of polymorphic type systems to XML data get confounded by the complexity of XML data and the conformance operator, resulting in type systems that are functionally limited and analytically expensive. The authors’ insight into this problem is to base type checking on data structure, rather than data operations, by using markings, which abstract XML document structure. Types can be checked using markings, insuring that the supplied data structure has the components required by the specified data structure. Under a set of reasonable but limiting technical assumptions, the type checking algorithms can be rendered as automata, suggesting that marking-based type checking is efficient.
This is not a paper for XML practitioners, not even those interested in having polymorphism in XML proper. By embedding XML in a functional language, the authors move their work into the realm of the language theoreticians, and it is not clear whether the work will find its way back to the practitioner’s realm in a useful form.