[TYPES] Purely functional programming with reference cells

[Eduardo León]

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