An algebra of mixin modules

Abstract

Mixins are modules which may contain deferred components, i.e. components not defined in the module itself, and allow definitions to be overridden. We give an axiomatic definition of a set of operations for mixin combination, corresponding to a variety of constructs existing in programming languages (merge, hiding, overriding, functional composition,…). In particular, we show that they can all be expressed in terms of three primitive operations (namely, stun, reduct and freeze), which are characterized by a small set of axioms. We show that the given axiomatization is sound w.r.t, to a model provided in some preceding work. Finally, we prove the existence of a normal form for mixin expressions.