Matching constraints for the lambda calculus of objects

Abstract

We present a new type system for the Lambda Calculus of Objects [16], based on matching. The new system retains the property of type safety of the original system, while using implicit match-bounded quantification over type variables instead of implicit quantification over row schemes (as in [16]) to capture Mytype polymorphic types for methods. Type soundness for the new system is proved as a direct corollary of subject reduction. A study of the relative expressive power of the two systems is also carried out, that shows that the new system is as powerful as the original one on derivations of closed-object typing judgements. Finally, an extension of the new system is presented, that gives provision for a class-based calculus, where primitives such as creation of class instances and method update are rendered in terms of delegation.