[TYPES] Purely functional programming with reference cells

[Jon Sterling]

Eduardo,

I would say that the kind of thing you are thinking about works
perfectly fine when you start from a typed computation system and then
classify it with a semantical type system, in the style of Nuprl. Then I
conjecture that a non-referentially-transparent operation is just
that—you can define it in the syntax of the computation system, but
because it is (by definition) not extensional, you cannot give it a
useful type.

For instance, consider an operation "X := λx. let y = @my-cell in
my-cell := x; y"; essentially, this operation spits out whatever input
you gave it *previously*. In order to give the type N -> N to this
operation, you have to show that "X=X:N-> N"; to prove that, you
demonstrate that "n:N !- [n/x]X=[n/x]X : N". But this is false, because
[n/x]X equals one thing on one side, and another thing on another side.
Therefore you have, in the sense of Bishop, an operation which is not a
function. A function is not just a lambda term, a function is a lambda
term which is "functional", and this is captured in the reflexive case
of the member equality judgement for the function type.

Another effect which is inevitable in an untyped computation system is
non-termination; and this also works fine in this semantical typing
discipline, since you show by induction that at each n, X(n)
terminates—and this is part of the typing derivation that you construct,
not part of the term.

I would say that the main point is that because each type in a
computational type theory is literally a PER over the terms of the
untyped computation system, then you can put whatever primitive effects
you want in the computation system, so long as you have given them an
operational semantics, and then define your type system over those such
that you have referential transparency in the typed terms.

A paper which may prove useful is Neel Krishnaswami recent "Integrating
Linear and Dependent Types"
(http://semantic-domain.blogspot.com/2014/11/integrating-linear-and-dependent-types.html).
Also see Bob Harper's "Constructing Type Systems over an Operational
Semantics"
(https://www.cs.uoregon.edu/research/summerschool/summer10/lectures/Harper-JSC92.pdf)
which seems to have inspired some of the choices that Neel made.

Kind regards,
Jon

On Wed, Nov 5, 2014, at 07:48 AM, Francois Pottier wrote:
> [ The Types Forum,
> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 
> Hello,
> 
> On Wed, Nov 05, 2014 at 05:55:59AM -0500, Eduardo León wrote:
> > 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. [...]  Furthermore, this also subsumes laziness as a special
> > case.
> 
> Just a little remark. I am not sure what you mean by "this subsumes
> laziness".
> In fact, it seems that if you want to implement "laziness" (that is,
> thunks)
> using reference cells, then you need to be able to write a value into a
> previously empty cell. So, you need to relax your condition and allow the
> new
> value to be "more defined" (in some sense) than the old value.
> 
> More generally, I think you might be interested by the paper "LVars:
> Lattice-based Data Structures for Deterministic Parallelism", by
> Lindsey Kuper and Ryan R. Newton.
> 
> Best regards,
> 
> -- 
> François Pottier
> Francois.Pottier at inria.fr
> http://gallium.inria.fr/~fpottier/