We present CMS, a simple and powerful calculus of modules supporting mutual recursion and higher order features, which can be instantiated over an arbitrary core calculus satisfying standard assumptions. The calculus allows expression of a large variety of existing mechanisms for combining software components, including parameterized modules similar to ML functors, extension with overriding as in object-oriented programming, mixin modules and extra-linguistic mechanisms like those provided by a linker. Hence CMS can be used as a paradigmatic calculus for modular languages, in the same spirit the lambda calculus is used for functional programming. We first present an untyped version of the calculus and then a type system; we prove confluence, progress, and subject reduction properties. Then, we define a derived calculus of mixin modules directly in terms of CMS and show how to encode other primitive calculi into CMS (the lambda calculus and the Abadi-Cardelli object calculus). Finally, we consider the problem of introducing a subtype relation for module types.

Type classes are a novel combination of parametric polymorphism and constrained types. Although most implementations restrict type classes to be single-parameter, the generalization to multi-parameter type classes has gained increasing attention. A problem with multi-parameter type classes is the increased possibilities they introduce for ambiguity in inferred types, impacting their usefulness in many practical situations. A new type-checking strategy, domain-driven unifying resolution, is identified as an approach to solve these problems. Domain-driven unifying resolution is simple, efficient, and practically useful. However, even with severe restrictions on instance definitions, it is not possible to guarantee that type-checking with unifying resolution terminates. This is in contrast with the naive generalization of single parameter resolution strategies. Domain-driven unifying resolution is guaranteed to terminate if the type class constraints are satisfiable; however satisfiability is undecidable even with severe restrictions on instance definitions. These results shed some light on ambiguity problems with multi-parameter type classes.

DrScheme is a programming environment for Scheme. It fully integrates a graphics-enriched editor, a parser for multiple variants of Scheme, a functional read-eval-print loop, and an algebraic printer. The environment is especially useful for students, because it has a tower of syntactically restricted variants of Scheme that are designed to catch typical student mistakes and explain them in terms the students understand. The environment is also useful for professional programmers, due to its sophisticated programming tools, such as the static debugger, and its advanced language features, such as units and mixins. Beyond the ordinary programming environment tools, DrScheme provides an algebraic stepper, a context-sensitive syntax checker, and a static debugger. The stepper reduces Scheme programs to values, according to the reduction semantics of Scheme. It is useful for explaining the semantics of linguistic facilities and for studying the behavior of small programs. The syntax checker annotates programs with font and color changes based on the syntactic structure of the program. On demand, it draws arrows that point from bound to binding occurrences of identifiers. It also supports α-renaming. Finally, the static debugger provides a type inference system that explains specific inferences in terms of a value-flow graph, selectively overlaid on the program text.