User loginNavigation |
Overlapping instances without chaosJ. 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.
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:
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. By Douglas McClean at 2010-12-31 00:03 | LtU Forum | previous forum topic | next forum topic | other blogs | 7283 reads
|
Browse archives
Active forum topics |
Recent comments
21 weeks 6 days ago
21 weeks 6 days ago
21 weeks 6 days ago
44 weeks 17 hours ago
48 weeks 2 days ago
49 weeks 6 days ago
49 weeks 6 days ago
1 year 3 days ago
1 year 5 weeks ago
1 year 5 weeks ago