Lambda the Ultimate

Resources, Concurrency and Local Reasoning, Peter O'Hearn, 2007.

Resource has always been a central concern in concurrent programming. Often, a number of processes share access to system resources such as memory, processor time, or network bandwidth, and correct resource usage is essential for the overall working of a system. In the 1960s and 1970s Dijkstra, Hoare and Brinch Hansen attacked the problem of resource control in their basic works on concurrent programming. In addition to the use of synchronization mechanisms to provide protection from inconsistent use, they stressed the importance of resource separation as a means of controlling the complexity of process interactions and reducing the possibility of time-dependent errors. This paper revisits their ideas using the formalism of separation logic.

I have to admit that in posting this paper, I was at least slightly motivated by the imp of the perverse -- it's pretty much a commonplace among expert programmers that reasoning about programs that use shared memory, explicit mutual exclusion, and concurrency is very difficult. So the urge to post a paper showing one approach for doing it in a clean (and imo quite beautiful) way was irresistible.

I recently came across the PML language, which aims to realize "the great unification between records/structures/modules/objects and functions/functors/methods". Sounds great, but it lead me to wonder exactly why there is a distinction between functions and functors in the first place.

Is this simply because in all current languages, the module language is separate from the term language? Does anyone have any references on functors that might clarify why functions and functors are currently distinct? Given the explanation of categories in the last link, I might hazard that functions are arrows/morphisms mapping objects within a single category, and functors map objects between different categories, ie. functions operate on objects within a category, functors on entire categories.

If that's accurate, then would "the great unification" involve reifying categories/modules at the term level somehow? If not, what does this "great unification" involve? The only reference to "functor" in the PML manual is on page 8:

/\id:a -> b : dependent types are allowed in PML. They are useful to write the type of functors: functions
that handle structures with type in their fields. Here is an example of such a dependant type with a value of
this type:
  type F = /\s:{ type p = [ A[] | B[] ] val q : p } -> s.p
  val f:F s = s.q

Any clarification is much appreciated. :-)