Denotational design with type class morphisms

LambdaPix technical report 2009–01

March 2009

Conal Elliott

Abstract

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 this 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. It also serves to transfer laws about a type’s semantic model, such as the class laws, to hold for the type itself. 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 types, meanings, and morphisms.

Paper (288K PDF, with minor revisions 2011/02/15)

See also:

BibTeX

@TechReport{Elliott2009-type-class-morphisms-TR,
  author      = {Conal Elliott},
  title       = {Denotational design with type class morphisms (extended version)},
  institution = {LambdaPix},
  url         = {http://conal.net/papers/type-class-morphisms},
  month       = {March},
  number      = {2009-01},
  year        = 2009
}

Errata

Errors and corrections are listed here as they’re reported and fixed.

2011–01–14: Most (all?) of the non-ascii characters below are somehow garbled when displayed from this web server. I don’t know what’s going on.

Version 2009/02/18

Thanks to Richard Smith, Tim Newsham, Ganesh Sittampalam, and Bas van Dijk for pointing out these mistakes.

Version 2009/02/20

Thanks to Patai Gergely and Phil Wadler for comments.

Version 2009/02/25

Version 2009/06/14

Thanks to Ivan Tomac for catching these mistakes.

Version 2009/10/16

Thanks to Noam Lewis for catching these mistakes.

Version 2009/11/21

Thanks to Nicolas Wu for these suggestions.

Version 2011/01/14

Thanks to adnap.

Version 2011/02/15

Thanks to augur.