Denotational design with type class morphisms
I’ve just finished a draft of a paper called Denotational design with type class morphisms, for submission to ICFP 2009. The paper is on a theme I’ve explored in several posts, which is semantics-based design, guided by type class morphisms.
I’d love to get some readings and feedback. Pointers to related work would be particularly appreciated, as well as what’s unclear and what could be cut. It’s an entire page over the limit, so I’ll have to do some trimming before submitting.
The 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 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.
You can get the paper and see current errata here.
The submission deadline is March 2, so comments before then are most helpful to me.
Enjoy, and thanks!
Dan Weston:
Enjoyed reading your draft of “Denotational design with type class morphisms”.
I think it would benefit the paper to mention (without explanation) categorical concepts as they apply. For instance, it seems that untrie (creating a suspension) is left adjoint to trie (deep seq). So hyperstrict would be the natural transformation epsilon. Also, section 1.11 seems like too much to tackle in a paper of this scope. You would need to explain the role of functor strength and costrength (aren’t those just the laws you listed in the seconnd equation there?) And the Hm. note begs for mention of a universal property.
It seems like the basic thrust of your argument is how to create a type class (interface) that is left-adjoint to the forgetful functor mapping an implementation to its denotational semantics (in the sense that any valid imstance must not only satisfy the meaning of the canonical instance but also have no extra meaning beyond it). This interface then (uniquely, up to isomorphism) tells “the truth, the whole truth, and nothing but the truth” about the abstract data type, which is effectively the above-mentioned epsilon natural trnansformation applied to the concrete data type. Words like this up front may help readers orient themselves.
Finally, the role of bottom seems to be central to the examples, with the goal of design to manifest the role of bottomn om the interface, instead of leaving each imstance free to treat it independently. Is this the main problem you see in interfaces today?
I notice you did not include Danielsson et al, 2006. “Fast and loose reasoning is morally correct.” in your references, but it seems relevant to your paper.
Also, in Related Work, you might consider Hagino’s dissertation 1987, “A Categorical Programming Language”. It seems to break functors into adjoint pairs (as I alluded to above) to more explicitly expose the role of strictness as I alluded to above. I may be way off base on this, because Hagino’s work is somewhat beyond my reach.
19 February 2009, 1:04 pmBas van Dijk:
Nice paper! Two small points I found so far (still reading…)
20 February 2009, 11:40 amI think the (a -> b -> c) in the type of ‘unionMb’ should be removed. (In the end of section 3 on page 3)
Shouldn’t the ‘ma’ and ‘mb’ be introduced in the lhs of the methods of the semantic instance Monoid (TMap k v) (In section 5, page 4)?
Philip Wadler:
I posted on this paper in my blog.
23 February 2009, 7:43 amConal Elliott » Blog Archive » Thoughts on semantics for 3D graphics:
[…] Recall that we’re looking for a semantics for 3D geometry. The type for Geometry might be abstract, with (->) being its semantic model. In that case, the model suggests that Geometry have all of the same type class instances that (->) (and its full or partial applications) has, including Monoid, Functor, Applicative, Monad, and Arrow. The semantics of these instances would be given by the corresponding instances for (->). (See posts on type class morphisms and the paper Denotational design with type class morphisms.) […]
22 November 2009, 11:42 pmConal Elliott » Blog Archive » Why program with continuous time?:
[…] been integral to FRP since the first incarnation as ActiveVRML. I’ve written several things recently about denotational […]
2 January 2010, 6:40 pmConal Elliott » Blog Archive » Is program proving viable and useful?:
[…] more examples of formally simple specifications, see the papers Denotational design with type class morphisms and Beautiful […]
2 January 2010, 7:22 pmMichał Ciaszczyk:
Hello! I have been thoroughly enjoying watching your talks on FRP and denotational design. This is fantastic work.
Since you seem to still update this paper occasionally, here’s a typo I noticed: In the end of section 5.2 on page 5, in the equation [[fmap f m]] = fmap f [[m]], I’m pretty sure fmap f [[m]] should be the composition fmap f ◦ [[m]] – so the expression can type check and be consistent with the following line.
30 December 2018, 8:24 pmConal:
Hi Michal. Thanks for the comment. I think that equation is as I intended. Writing “
⟦m⟧” instead as “μ m” may help clarify. Then