[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hello: I am trying to reconcile "impure" language features with the benefits of purely functional programming: equational reasoning, getting theorems for free from parametric types, just-flip-a-switch parallelism, etc. Right now, the feature I am focusing on is ML's reference cells. I would like some feedback on whether my approach makes sense. As far as I can tell, the essence of purely functional programming is captured by referential transparency: For values "f", "g", "x", "y", whenever "f = g" and "x = y", "f x" and "g y" must both evaluate to equal values or both diverge, if they type check. (I am really tempted to consider non-total functions to be non-values here.) In a language like Haskell, or rather, some idealized subset of it (no seq, no bottom), we begin with a fixed notion of term equality (completely unrelated to the Eq type class) and then guarantee by construction that referential transparency holds as a metatheorem. However, this approach to defining equality is too inflexible to be useful. For example, if I implement priority queues as binomial heaps, it is perfectly possible for two heaps to be balanced differently internally, yet have the same elements and thus be equal *for all I care*. So I want to take a different approach: Rather than committing myself to a fixed notion of equality, let's start with the notion of referential transparency as *definitionally* true in the metatheory. Then, equality is the smallest equivalence relation between values that makes referential transparency hold. I think this gives us a beautiful account of reference cells, one that does not force us to call them "non-functional features": Every time we update a reference cell, we are asserting that the old and new values are equal. (In ML, with the caveat that we do not provide any more justification for this assertion than "because the programmer says so".) Furthermore, this also subsumes laziness as a special case. Does this make sense? This idea of "mutation as an identification between old and new values" somehow reminds me a lot of the role of paths in homotopy type theory. Is this intuition correct? -- Eduardo León
