Variations on Abstracted Sets

The standard OCaml library includes the Set functor (Ocaml’s set module (from .ml and .mli, described here)) which takes a module describing aspects of things you want to collect in sets, and supplies a module that provides tools for manipulating sets composed of those objects. This code does this trick for integers. The module IP therein is all that Set needs to know about integers; how to compare two of them. To be obscure we tell the code to sort the integers putting odd integers first. This explores a style variation on the same where the integer module is anonymous.

The code for Set was compiled in an environment where the type of the set elements was a parameterized type name, ‘t’, and the only operation available on that type is ‘compare’.

That is not a very plausible secret to keep so we advance to sets of pairs of integers and strings where we compare two pairs by comparing their integer parts. This code defines module PS to compare two pairs by examining their integer first parts. Two pairs with the same first element are considered as equivalent and only the first is kept. The function ‘PS.elements’ takes such a set and returns a list of its elements in sorted order.

This security relies on the lack of reflection in OCaml. This sort of security presumes some sort of assurance that the library modules and the modules that they use recursively do not include C modules. A C module, coded to the standards can discover, at run time, the constituent parts of the set elements. Standard modules Obj and Marshal must thus be recursively excluded. I.E. the library must itself be confined. Emily does this. See this.

I experiment here to verify some comments above that are actually guesses. This section of the OCaml manuals describes relations between file names and module names. It is not obvious.

Mark Miller tells me that the property that I hopefully and mistakenly attributed to OCaml’s modules is called ‘parametricity’. This paper seems to be a good description of the etymology of “parametricity” and describes how several papers successively honed the notion until it became precise. Strachey coined the term and gave examples of routines that had and did not have parametricity. Strachey gave no precise demarcation. This may be notes from Strachey’s lecture that introduced the concept. I enjoyed the paper but it does not mention parametricity. The Wikipedia article quotes names but gives no hint of what it is. The reynolds paper ...

A thought