Objects in many programming languages are indexed by first-class strings, not just first-order names. We define λob (“lambda sob”), an object calculus for such languages, and prove its untyped soundness using Coq. We then develop a type system for λob that is built around string pattern types, which describe (possibly infinite) collections of members. We define subtyping over such types, extend them to handle inheritance, and discuss the relationship between the two. We enrich the type system to recognize tests for whether members are present, and briefly discuss exposed inheritance chains. The resulting language permits the ascription of meaningful types to programs that exploit first-class member names for object-relational mapping, sandboxing, dictionaries, etc. We prove that well-typed programs never signal member-not- found errors, even when they use reflection and first-class member names. We briefly discuss the implementation of these types in a prototype type-checker.
We have a series of blog posts that present a high-level overview of this paper (Post 1, Post 2, and Post 3).
@inproceedings{politz:fcfn,
author = "Joe~Gibbs Politz and Arjun Guha and Shriram Krishnamurthi",
title = "Semantics and Types for Objects with First-Class Member Names",
booktitle = "Foundations of Object-Oriented Languages",
year = 2012
}