Semantics and Types for Objects with First-Class Member Names (FOOL '12)

[brianhempel]

Joe Gibbs Politz, Arjun Guha, Shriram Krishnamurthi (FOOL '12)

Objects in many programming languages are indexed by first-class strings, not just first-order names. We define λSob (“lambda sob”), an object calculus for such languages, and prove its untyped soundness using Coq. We then develop a type system for λSob 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.

https://cs.brown.edu/~sk/Publications/Papers/Published/pgk-sem-type-fc-member-name/paper.pdf