One Module to Rule them All

By Scott

Hey all, Friday night we covered chapter 42 of PFPL on Modularity and Linking, which divided up into several interesting but connected discussions.

Next Friday will be chapter 43 on Singleton Kinds and Subkinding in the usual time and place, 6:30pm at Bento Miso.

Modularity is that thing that every developer says their design has, but in practice modular code can be as elusive as a Jackalope. In this chapter, Harper boils away the unnecessary concepts leaving just the bare essentials for modularity, namely substitution and a type signature for the API. The type signature specifies a clean type-safe boundary between modules and substitution is what lets you put the code back in the right place.

Harper uses the metaphor that APIs can then be used a bit like lemmas in a mathematical proof, providing convenient shorthand for an earlier derivation that gets used frequently. This metaphor gets really interesting though if you take into consideration the Propositions as Types isomorphism; which means that an API isn’t just like a lemma in mathematics, it is a lemma!

Linking is the important implementation glue that lets you take advantage of all this modularity andHarper outlines a number of different approaches and some of their strengths and weaknesses. I found the Cardelli paper, [Fragments, Linking, and Modularization] (http://lucacardelli.name/Papers/Linking.A4.pdf) to be a good resource to read more in depth about the Linking process.

Until next week, Scott