Numerous programming and schema languages contain the notion of value types. However, support for value space-based subtyping is spotty. This paper presents a formal type system for atomic value types as an extension of the simply typed lambda calculus with subtyping. In the λC-calculus, value types can be derived through the application of value space constraints. Type inference rules can be used to infer transient value space constraints that hold for limited scopes of a program. The type system of the λC-calculus is proved to be sound. The λC-calculus was fully implemented in Java and C#. The presented approach was successfully validated to subsume XML Schema Definition type construction and to facilitate the integration of XSD data types with the C# programming language.
Download PDF (draft).
Related approaches (list is unordered and not exhaustive):
- Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken. "Flow-sensitive type qualifiers.", pdf
- Brian Chin, Shane Markstrum, and Todd Millstein. "Semantic type qualifiers.", pdf
- Brian Chin, Shane Markstrum, Todd D. Millstein, and Jens Palsberg. "Inference of user-defined type qualifiers and qualifier rules.", pdf
- David Greenfieldboyce and Jeffrey S. Foster. "Type qualifier inference for Java.", pdf
- ...
No comments:
Post a Comment