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.
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 ...