Denotational design with type class morphisms

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 (436K PDF, with minor revisions 2010/01/07)

Errata

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

Version 2009/02/18

Section 1, page 1, “essense” should be “essence”
Section 3, page 3, “lookup m k = Map.lookup m k”: the Map.lookup should be TMap.lookup.
End of Section 3, page 3. Remove “(a → b → c) →” in the type of unionMb should be removed.
Section 5.1. “μ (⊕) = …” should read “μ (ma ⊕ mb) = …” in the second and third occurrances
Section 5.2, page 4, “λ → μ m k” should be “λ k → μ m k”
5.4: “liftA2 h u v = fmap h (∗) u (∗) v” should be “liftA2 h u v = fmap h u (∗) v”
Section 9.1, page 8 “5 ∗ sqrt f, which can mean λ x → sqrt (f x)”. Insert “5 ∗” before sqrt.
Section 9.3 “In this context, there a”: Insert “is” between “there” and “a”.

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

Version 2009/02/20

Abstract, last sentence: “examples of type” becomes “examples of types”
Replace the confusing use of calligraphic M with semantically-bracketed type, “⟦C⟧”.
I’ve also replaced “μ” with semantic brackets, e.g., “μ (fmap f) m” becomes “⟦fmap f m⟧”. I’d like some reader feedback on this change.
On the bottom of page 2, the type of mu contains an “=” sign, meant to be a “→” instead.
Fixed accent on Saint-Exupery.
Page 3, add type of ⟦⋅⟧ for TMap.
Page 3, “different key types” should be “different value types”.
Section 4, second paragraph, change TMap to Map.
Section 9.3.4, definition of Result: change “[String]” to “String”.
Page 11, Section 10, “let’s look a simpler setting of” changed to “let’s look at a simpler setting:”.

Thanks to Patai Gergely and Phil Wadler for comments.

Version 2009/02/25

Page 3, end of section 3, rename “unionMb” to “union”.

Version 2009/06/14

Reference: Push-pull functional reactive programming
Page 1, second paragraph of second column, “yielding Nothing where undefined” should be “yielding ⊥ where undefined”.
Page 3, third paragraph, “factor our” becomes “factor out”.

Thanks to Ivan Tomac for catching these mistakes.

Version 2009/10/16

Section 3, first paragraph, “deeply Benefits”. Interposed period.
Section 4 paragraph 3, “It’s straightforward to show …”. Removed accidental self-citation in extended version.
Section 4, the proof of [ma ⊕ ∅] ≡ [ma]. “semantics of Nothing” should be “semantics of ∅”
Section 10.1, in proof of morphism for f + g: “[[liftA₂ (+) f g” is missing its closing “]]^x”, which then shows up in the last line of the proof.
Section 10.1 proof of fmap, “{ (!*?) on functions }”: the “(!*?)” should be star in circle.
Section 10.1, right after the f + g, “Funtor” is missing a ‘c’.
Section 10.1, in proof of Functor and Applicative morphisms, two references to “[[.]]” should be “[[.]]^x”.
Section 11, after the definition of foldr: “There is also strict variant…”. Missing ‘a’.

Thanks to Noam Lewis for catching these mistakes.

Version 2009/11/21

Section 4, instance Monoid (First a): Use “l” for left argument and to (⊕) and “r” for right argument.
Section 7, paragraph 3: “These failures again looks like bad news.” becomes “Again, these failures look like bad news.”

Thanks to Nicolas Wu for these suggestions.

Denotational design with type class morphisms

LambdaPix technical report 2009–01

March 2009

Conal Elliott