ICFP’96 - Mixin Modules

Mixin Module Syntax

structure M = 
   mixin <defns1> -- prelude: type, function and module definitions
   body <defns2> -- the part assumed to be recursive, can use <defns1>
   init <defns3> -- initialization section: 
                 -- where <defns1> and <defns2> are visible
end

signature S = 
   mixinsig <decls1>
   body <decls2>
   init <decls3>
end

• composition rule for mixin modules & signatures
• equality theory for signatures with mixin compositions
• closure of mixin → SML signature
• mixin can occur inside functor bodies and arguments

An extension we do not consider is mixin functors, mixins which may be combined and closed into a functor. We leave this for future work.

Examples

2.1 Simple Interpreter Mixins

• the use of inner function to refer to the final composition

fun eval (CONST i) . = NUM i 
  | eval tm (e:env) = inner tm e

• This is in contrast to Encoding CP with distributive recursive types - refined, where the behaviour of merge is pre-configured to be such passing the inner call

idea to see what mixin module configure for negative positions might suggest how to deal with merge in the context of CP #question Is Mixin Modules true regarding below according to Compositional Programmin?

The fundamental difference between traits and mixins is the way of dealing with conflicts when composing multiple traits/mixins. Mixins implicitly resolve the conflicts according to the composition order, whereas the programmer must explicitly resolve the conflicts for traits.

2.2 Cyclic Import Dependencies

To illustrate the problem, the authors use a real example from the SML of New Jersey (SML/NJ) compiler.

• The Scenario: A “type explanation” facility was added to the compiler’s type-checker. This feature needed to store extra information in the compiler’s data structures for types.

• The Cycle: This created a circular dependency:

  1. The Types module (defining data types for the language) now depended on the TypeExplain module to handle the explanation data.
  2. The TypeExplain module needed to know about the abstract syntax trees, making it a client of the Absyn module.
  3. The Absyn module (defining abstract syntax) inherently depends on the Types module.

• The Result: This formed an import cycle: Types → TypeExplain → Absyn → Types.

• Undesirable Workarounds: The developers had to choose between two poor solutions:

  • Using unsafe type casting, which is a hack that breaks the safety of the type system.
  • Merging the Types, Variable, and Absyn modules into a single “mega-module”. This solves the dependency issue but harms the compiler’s architecture by destroying modularity.

Why Existing SML Tools (Functors) Fail

The authors then address a potential counter-argument: couldn’t this problem be solved using functors (SML’s parameterized modules)?. The answer is no. Using functors merely delays the problem until the point where the modules are instantiated. To create the final Types, TypeExplain, and Absyn structures, you would need to apply the functors to each other. This leads to the exact same circular dependency at the instantiation site, as their definitions remain mutually recursive.

What about Modula-3?

• achieved by rational trees and circular unification
• reduced type error detection
• complex inferred type

The Proposed Solution: Mixin Modules ✨

The paper argues that mixin modules provide an elegant solution by introducing a new form of module composition based on “merging” the fixed points of recursive definitions rather than function application.

• How it Works: The Types, TypeExplain, and Absyn components would be declared as separate mixins.
• Placeholder Definitions: The Types mixin can declare a placeholder for the explanation data structure (e.g., datatype explain;) without fully defining it. This is enabled by a minor extension to ML allowing empty datatype definitions.
• Merging Definitions: The TypeExplain mixin provides the actual constructors for the explain datatype. When these mixins are composed, their partial definitions are merged into a single, complete datatype.
• Mutually Recursive Functions: This merging also applies to functions. A function copyTy in the Types mixin can call a function copyExplain that will be defined later in the TypeExplain mixin, because they are ultimately combined into a single group of mutually recursive functions.

2.3 Parametric Overloading and Generic Functions

“Type classes remain the main performance bottleneck in Haskell” (Duggan and Sourelis, 1996, p. 3) Is it still true nowadays?

• See Dominic Duggan and John Ophel. On type-checking multiparameter type classes. for encoding mult that works on various combinations (e.g., vector-vector, scalar-vector) with mixin modules
• Other extenions of parameteric overloading (I think w.r.t. type classes) are also available
  • type constructor classes
  • n.b. homogeneous vs. hetrogeneous data strutures, CLOS generic functions
    • related to the issue of subclassing (Section 5)

Static semantics of mixin modules

Formal Syntax

Simplifications

• Functor applications are only allowed for paths
  • may assume a translation from a more liberal source language
• each functor takes a single argument
• …