Wadler's Blog

I've edited my post to correct the spelling of Conal's name (profuse apologies, Conal!) and to improve the tone (on rereading I thought my remarks came across as too negative).
 

Hi Phil,

Thanks for the comments, including the reminder of John Reynolds's paper.

Yes, there's certainly an overlap with my unpublished "Simply efficient ..." paper (unsuccessfully submitted to last year's ICFP). Since noticing the TCM pattern in that context, I've been seeing it much more, and I expect there would be interest in an exposition not wrapped up in FRP. I've tended to write idea-dense, rather than example-dense, papers, and perhaps your prefer reading them. This time, I thought I'd give a go at more examples, so the TCM idea gets across more effectively and hopefully has some impact in programming practices.

As for your comment on my remarks about the applicative functor laws coming for free for TMap, I agree and disagree. Yes, the laws are 'for free' thanks to having been verified for the semantic model (->). What this observation means is that library designers get to re-use work that has already been done with some very well-studied mathematical types like functions, sets, pairs and sums. It's not just a lucky coincidence that my semantic model has been explored and shown to have useful properties, including class laws. Rather, I chose this semantic model in part because it's so familiar and broadly useful that it's a basic part of my mental vocabulary when I ask myself what things mean.

So this is the advice I'm trying to convey in this paper: when designing a library, innovate in your implementations, and relate to precise and familiar semantic models. Implementing those models faithfully guarantees that your library's users will get simple semantics and expected properties, in addition to whatever performance benefits you provide.

As for applicability of the TCM principle, I disagree with your conclusion, because isomorphism of type and model is not necessary or even helpful, in order for the class laws to come for free. For instance, the TMap type is finite maps, while its model is general functions. Similarly, the "Simply efficient ..." paper gives the example of "reactive values", whose semantics model is function of time, while the meaning of a reactive value is always a discretly-changing (step) function. I see importance in the lack of requirement for surjectivity: the larger semantic model can have simpler structure. And there is a much better chance of finding a simple model with nice properties if the modeled type is free to map to a subset of the model. I will make this point clearer in the paper. Thanks.
 

A correction to my previous comment: the meaning of TMap (i.e., the semantic function's codomain) is not finite maps, as I'd said, but rather maps with finitely many distinct elements. Again, not the whole model, so TMap and (->) are not isomorphic. In some other examples, the difference between type and model are more pronounced.

I think your "oversells" assessment came from a mistaken understanding that class laws coming for free depends on an isomorphism of type & semantics. Do you think so also? I'd like to make sure I'm not missing something.
 

The difference between (TMap a b) and (a -> b) in the paper was not very clear to me. The claim that the desired properties of TMap came 'for free' struck me as an overclaim because all of the hard work of the proof was required, but performed on the type (a -> b) instead. If this technique really yields any significant savings in work then that needs to be clarified, as it certainly was not clear to me when I read the paper.
 

Thanks, Phil.

Now I think there were two distinct communication glitches, which I can hopefully prevent in the version I submit to ICFP.

First, I didn't mean to suggest that the class laws came 'for free'. But rather that they were guaranteed to hold, thanks to the semantic model satisfying those laws. (In the context of a type class morphism, the model always satisfies the class laws, since the morphism maps instance to instance).

When you described TMap and (->) as isomorphic, I thought you believed that the guaranteed class laws depended on type/model isomorphism, which would indeed limit their applicability. But now I'm not sure the isomorphism piece was relevant. Maybe your comment was just about ease and not breadth of applicability.

I'll claim something close to "for free", which is "already paid for". Often, for a simple and fitting semantic model, someone already has done the hard work of verifying class laws, so the library designer can smile and accept the gift. When the model is unusual or complex enough that the work has not been done, it may be that (a) the model can be improved or (b) someone can do the hard work for the model and share it with others. I think what's behind this "already paid for" idea is my belief that good semantic models can be reused.

Sound right to you?

Thanks very much for the feedback!
 

That works for me. 'Already paid for' fits the bill in a way 'for free' does not.