[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 > [email protected] > http://gallium.inria.fr/~fpottier/
