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