Denotational design with type class morphisms. Conal Elliott.
Type classes provide a mechanism for varied implementations of standard interfaces. Many of these interfaces are founded in mathematical tradition and so have regularity not only of types but also of properties (laws) that must hold. Types and properties give strong guidance to the library implementor, while leaving freedom as well. Some of the remaining freedom is in how the implementation works, and some is in what it accomplishes.
To give additional guidance to the what, without impinging on the how, this paper proposes a principle of type class morphisms (TCMs), which further refines the compositional style of denotational semantics. The TCM idea is simply that the instanceâ€™s meaning is the meaningâ€™s instance. This principle determines the meaning of each type class instance, and hence defines correctness of implementation. In some cases, it also provides a systematic guide to implementation, and in some cases, valuable design feedback.
The paper is illustrated with several examples of type, meanings, and morphisms.
To continue in our new all-Conal format... This paper brings together a bunch of things that Conal's been talking about lately, and "algebra of programming" fans will probably like his approach.
(I have a hunch that what he calls a "type class morphism" could be described using standard categorical jargon, but I haven't given it much thought. Suggestions?)
Recent comments
37 min 56 sec ago
4 hours 50 min ago
5 hours 7 min ago
5 hours 14 min ago
5 hours 25 min ago
5 hours 36 min ago
12 hours 32 sec ago
12 hours 27 min ago
12 hours 56 min ago
15 hours 4 min ago