[TYPES] Purely functional programming with reference cells

[Jon Sterling]

(Sorry, please read the first sentence as “from an *untyped* computation
system" not "typed".
-JMS

On Wed, Nov 5, 2014, at 09:01 AM, Jon Sterling wrote:
> 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/