Lambda the Ultimate

J. Garrett Morris and Mark P. Jones from Portland State University published a paper on type classes that I've not seen mentioned here. In Instance Chains: Type Class Programming Without Overlapping Instances they describe a system which permits and formalizes several useful examples of type class instances that would overlap according to the Haskell-style rules.

This paper describes a new type class system, implemented in a prototype tool called ilab, that simplifies and enhances Haskell-style type-class programming. In ilab, we replace overlapping instances with a new feature, instance chains, allowing explicit alternation and failure in instance declarations. We describe a technique for ascribing semantics to type class systems, relating classes, instances, and class constraints (such as kind signatures or functional dependencies) directly to a set-theoretic model of relations on types. Finally, we give a semantics for ilab and describe its implementation.

In synopsis, the basic approach is to allow declaration of "chains" of instances declared within one module to overlap within the chain. The open nature of type classes is preserved by keeping the Haskell-style overlap rules forbidding overlap between chains, several chains in several modules may declare instances of the same class. By supporting negative proofs of class membership, and by ordering instance axioms within chains, they are able to maintain the uniqueness-of-evidence condition required by the translation mechanism described in Jones's earlier (and awesome) work on Qualified Types: Theory and Practice. This negative information also provides a simple facility for closing type classes in cases (like arithmetic functions of type-level naturals) where the rules for class membership are generative and the open nature of type classes hinders us by leaving open the possibility that someone will add unexpected and nonsensical instances. The paper covers both multi-parameter type classes and functional dependencies, which makes the described system very practical and expressive.

Among the applications of overlapping instances typed (and given a formal semantics, which is another nice feature of the paper) by this approach, are:

• Swierstra's functional pearl on Data Types a la Carte which uses overlapping instances to simplify injection of terms into coproducts of functors
• Type level Peano arithmetic after Hallgren's Fun with Functional Dependencies
• Type-specific redefinitions of polymorphic functions where the polymorphic implementation might be unacceptably slow, etc.

The example of Swierstra's construction is the interest that led me to this paper. The approach described in section 6 of that paper appears (from my amateur perspective) to offer a promising solution to the "the IO monad is a disorganized dumping ground for all kinds of effects"-problem. I want types for database stored procedures expressive enough that the portion of their effects relevant to optimization and to security policy can be explained (and composed!) in terms of the type system as opposed to another layer of semantic rules (composed only by recursive examination of the implementation of every procedure you call...) constraining use of library functions which introduce non-determinism (clocks, PRNGs, details about the client who initiated a request, various sorts of partiality, local file system access, catalog operations, system maintenance / support functions, access to performance and indexing information, etc). I suspect that with type-level identifiers for relation variables, it might even be possible to encode which relvars are consulted/updated by a procedure, thereby tackling another set of security semantics within an existing and well-understood machinery for static analysis.