Re: Again: Referential Equality
On 28-Jul-1999, Lennart Augustsson [EMAIL PROTECTED] wrote:
Fergus Henderson wrote:
equal x y = unsafePerformIO $ do
ptrEq - ptrEqual x y
return (ptrEq || deep_equals x y)
Note that unlike `req', `equal' here _is_ referentially transparent.
No, it's not. If x and y are both bottom you can get unexpected
results, i.e., sometimes it terminates, sometimes it doesn't.
Sorry, you're absolutely right. And the same problem arises with
exceptions too -- if x and y are both `raise "oops"' then sometimes it
returns `True' and other times it returns `raise "oops"'. Oops indeed!
I'm not sure off-hand what the best fix would be. One possible solution
would be to force evaluation of the arguments if they are equal:
equal x y = unsafePerformIO $ do
ptrEq - ptrEqual x y
return (if ptrEq then x `hyperseq` True else deep_equals x y)
However, this compromises the nice O(1) performance in that case.
Another possible fix would be to rename `equal' as `unsafe_equal',
noting that it is referentially transparent so long as neither of its
arguments contains bottom or any exceptional value; it would then be
the programmer's responsibility to check that all callers ensure that
this condition is satisfied for all calls to `unsafe_equal'.
The second fix is probably best. But it's still rather ugly.
P.S.
I'm just glad that the same problem doesn't arise in Mercury :-)
The analagous Mercury code would be
:- type bool --- yes ; no.
:- func equal(T, T) = bool.
:- func deep_equals(T, T) = bool.
:- pred ptr_equal(T::in, T::in, bool::out) is cc_multi.
equal(X, Y) = promise_only_solution((pred(Res::out) is cc_multi :-
ptr_equal(X, Y, PtrEq),
( PtrEq = yes, Res = yes
; Res = (if deep_equals(X, Y) then yes else no)
)
)).
In Mercury, for cases such as `equal(throw("oops"), throw("oops"))'
or `equal(loop, loop)' (where `loop' is defined by `loop = loop.'),
the declarative semantics says that the result must be `yes'. The
operational semantics, however, exhibits the same nondeterminism as
the Haskell code did. This is OK in Mercury because in Mercury
although the operational semantics is required to be sound w.r.t. the
declarative semantics, it is not required to be complete; in cases
where the declarative semantics says that the result is `yes', it may
still be acceptable for the implementation to throw an exception
rather than computing the result `yes'. In Mercury, if you want to
reason about whether your program will terminate or throw exceptions,
you need to use the operational semantics rather than the declarative
semantics.
--
Fergus Henderson [EMAIL PROTECTED] | "I have always known that the pursuit
WWW: http://www.cs.mu.oz.au/~fjh | of excellence is a lethal habit"
PGP: finger [EMAIL PROTECTED]| -- the last words of T. S. Garp.
Re: Again: Referential Equality
At 14:11 +0200 1999/07/27, Koen Claessen wrote: The contructs we add to the language are: type Ref a = ... ref :: a - Ref a deref :: Ref a - a (=) :: Ref a - Ref a - Bool This basically gives you ML-style but non-updatable references, but you can compare them for equality. You can also see it as pointer equality, but only on objects of a certain type, so that you have to explicit at creation time if you want to pointer-compare them later. let x = ref 27 in x = x yields True, whereas ref 27 = ref 27 yields False. I think there is not a big problem with breaking "referential transparency"; the same think happens in pure math often and it is part of a normal procedure of constructing mathematical objects: Referential transparency means that if a = b then F(a) = F(b), where "=" is semantic equality But "=" is in reality just one of several different possible equivalence relations. Let's rewrite it with an arbitrary equivalence relation x ~ y. Then it says if a ~ b then F(a) ~ F(b) In other words, one focuses on the semantic function objects F which are homomorphisms with respect to the equivalence relation ~. Take an example: construct say the real numbers R as the Cauchy sequences of rational numbers Q modulo the equivalence relation that two sequences have the same limit (omitting boring mathematical details). Then a lot of different Cauchy sequences of rational numbers will represent the same real number. (So this corresponds roughly to different references of the same semantic object in a computer language.) In this case if a ~ b then F(a) ~ F(b) simply means that it is a well defined real valued function. But it does not prevent a mathematician to consider all Cauchy sequences in such a construction, and functions which do not satisfy if a ~ b then F(a) ~ F(b) One might guess that for a general purpose use, these are the interesting functions, but that is all. So the two conditions if a `eq` b then F(a) `eq` F(b) if a `req` b then G(a) `req` G(b) will only lead to different classes of functions (homomorphisms with respect to different properties). The latter will in math more correspond to consider all underlying set functions, whereas in the former case one restraints at preserving certain semantic structure. So I think one should not bother too much about breaking referential transparency when allowing access to the underlying runtime covers. On the contrary, it seems that this exactly what one should expect to happen. (One might guess that the referential transparency concept pops up in functional language, because it somehow is important in constructive math. Then it is interesting that the approach break down in describing all the innards of the runtime object of a computers. Perhaps this is a weak spot of constructive math relative traditional math, then.) Hans Aberg * Email: Hans Aberg mailto:[EMAIL PROTECTED] * Home Page: http://www.matematik.su.se/~haberg/ * AMS member listing: http://www.ams.org/cml/
RE: Again: Referential Equality
So the two conditions if a `eq` b then F(a) `eq` F(b) if a `req` b then G(a) `req` G(b) will only lead to different classes of functions (homomorphisms with respect to different properties). The latter will in math more correspond to consider all underlying set functions, whereas in the former case one restraints at preserving certain semantic structure. So I think one should not bother too much about breaking referential transparency when allowing access to the underlying runtime covers. On the contrary, it seems that this exactly what one should expect to happen. I would not be so gung-ho about breaking referential transparency. While I agree that it is convenient in specific cases to have a language that doesn't obey referential transparency, and just use a different, more specialized theory for reasoning about programs, it seems like that strategy would force one to deal with either one complex, monolithic theory, or a multiplicity of similar smaller theories. The way Haskell employs monads, we can define what amounts to a domain-specific sublanguage which maybe isn't referentially transparent, and then translate propositions about programs in the sublanguage into more familiar propositions about Haskell programs which are referentially transparent. So Haskell functions as a universal language to express domain-specific language denotations in. That was the whole point of introducing monads in the first place, I think: compositional denotational semantics. So, why would you want to break referential transparency when you've gone to all the above trouble to preserve it already? --FC
Re: Again: Referential Equality
On 27-Jul-1999, Andreas C. Doering [EMAIL PROTECTED] wrote: [Simon Peyton-Jones wrote:] [Andreas Doering wrote:] let x=[1..] in x==x would not terminate in the first case but succeed in the second. But, much worse let x = (a,b) in x `req` x = True but (a,b) `req` (a,b) = False So referential transparency is lost. This is a high price to pay. You are right that *something* is needed; but I don't yet know what. I agree that `req' is not the right primitive. But unfortunately that didn't stop it from being included in the ghc extensions library! (ghc calls it `unsafePtrEq'.) This is a design bug in the ghc, IMHO, and it ought to be changed. Instead of providing unsafe primitives such as `req', or `unsafePtrEq', which can never be used in ways that can be guaranteed to be safe against all possible compiler optimizations that assume referential transparency, it's better to provide safe equivalents, by putting them in an appropriate monad. In this case what is desired is a nondeterminism monad. The `IO' monad will suffice as a nondeterminism monad, since it provides nondeterminism as well as I/O, but it's not really ideal, because in this case we only want the nondeterminism rather than the I/O. Using the `IO' monad works, but it doesn't do a good job of documenting the properties of the function. I do not think that this is "worse". Such a funtion would have to be used wise. In most circumstances the most wise use of such a function would be to not use it at all, IMHO! A compiler might make optimizations based on the assumption that all functions are referentially transparent, and so if functions such as `req` are not referentially transparent, then these optimizations would be based on incorrect assumptions, and could therefore lead to undefined behaviour, potentially including segmentation faults or worse. As it happens, I can't think of any good examples of this off-hand. But I'm sure such examples could be constructed. "True" means "Sure both terms are equal, we can save further actions" "False" means "Do not know," It is a primitive which has to be used as in the list comparison. Then, "referential transparency" is recreated, but the termination problem remains. In circumstances where you have an `impure' function which is used in a manner which is pure, you should enclose such uses inside `unsafePerformIO' or something equivalent. This is a *safe* use of `unsafePerformIO'. Currently the Haskell report does not document `unsafePerformIO' and does not state which uses are safe, but IMHO this is a bug in the current Haskell report. Note that there is a big difference between using a primitive which can never be guaranteed to be referentially transparent, like `req', and using a primitive like `unsafePerformIO' which *is* safe and referentially transparent when used in an appropriate manner. With the former, you can never be sure that the compiler won't mis-optimize your code. Meanwhile Jeff Lewis has a BDD library accessible from Haskell, I believe. [EMAIL PROTECTED] I will ask him. I made a BDD-lib already, but it uses an array to store the nodes, and garbage collection is explicitely programmed on this array requiring reallocation, contents copying and so forth, very ugly. Certainly using an array type for this, with the resulting need to do manual garbage collection, is very ugly. You should use a type which matches your needs. Such types do exist. For instance, the ghc stable name type is sufficient; an IO-monad version of the `req` operator that you wanted can be implemented as import Stable x `ptrEqual` y = do x_name - makeStableName x y_name - makeStableName y return (x_name == y_name) However, the ghc stable name type might impose more overhead than you need for this application -- e.g. ghc might not be able to optimize the above code to the simple pointer comparison that you would like. -- Fergus Henderson [EMAIL PROTECTED] | "I have always known that the pursuit WWW: http://www.cs.mu.oz.au/~fjh | of excellence is a lethal habit" PGP: finger [EMAIL PROTECTED]| -- the last words of T. S. Garp.
Re: Again: Referential Equality
On 27-Jul-1999, Frank A. Christoph [EMAIL PROTECTED] wrote: I would like to have a comparison instruction that compares the internal reference of two objects. Let's call it "req". req :: a - a - Bool By coincidence, I was just looking at GHC's documentation on stable names and pointers, and it seems relevant here. http://research.microsoft.com/users/t-simonm/ghc/Docs/latest/libraries/libs- 14.html Something like this might do the job for you: req a b = unsafePerformIO $ do a' - makeStableName a b' - makeStableName b return (a' == b') This is an unsafe use of unsafePerformIO, because `req' is not referentially transparent. Instead, you should use ptrEqual :: a - a - IO Bool ptrEqual a b = do a' - makeStableName a b' - makeStableName b return (a' == b') and the call to unsafePerformIO should be moved outwards, into the caller, to the point at which referential transparency is preserved, e.g. equal x y = unsafePerformIO $ do ptrEq - ptrEqual x y return (ptrEq || deep_equals x y) Note that unlike `req', `equal' here _is_ referentially transparent. -- Fergus Henderson [EMAIL PROTECTED] | "I have always known that the pursuit WWW: http://www.cs.mu.oz.au/~fjh | of excellence is a lethal habit" PGP: finger [EMAIL PROTECTED]| -- the last words of T. S. Garp.
Re: Again: Referential Equality
On 27-Jul-1999, D. Tweed [EMAIL PROTECTED] wrote: On Tue, 27 Jul 1999, Simon Marlow wrote: req a b = unsafePerformIO $ do a' - makeStableName a b' - makeStableName b return (a' == b') That's exactly what to use in a situation like this. Pointer equality loses referential transparency in general (as Simon P.J. pointed out), hence the use of the I/O monad in our Stable Name API. Furthermore, if you intend to encapsulate your use of pointer equality in a "safe" abstraction, say a memo table, then use of unsafePerformIO is entirely justified. The req function above is of course an "unsafe" abstraction, because it exposes the representation of a and b. Just an idle curiousity question: when you say it loses referential transparency am I right in saying it this is only with respect to compile time transformations ( program proofs,etc) but that there's no problem _for a given compiled program_ about req a b changing it's value depending upon the way demand drives the lazy evaluation reduction strategy, or is there a subtlety there? It's not necessarily just compile time transformations. Imagine an implementation which checks referential transparency at run time (e.g. using techniques similar to those used for memoization). A program using `req' could fail such checks. (I'm just curious about the use of the IO monad, which regulates things which depend on the an underlying state which may change with time in a difficult to predict way depending on the precise pattern of reduction, rather than say a `compile time monad'.) You're right that using the `IO' monad for this is misleading. Using a nondeterminism monad (e.g. the NDSet type that I posted to this mailing list about a year ago) would be clearer. But the use of `IO' is sufficient to make things referentially transparent; the choice of whether to use `IO' or a more specific nondeterminism monad is an issue of programming style rather than one of correctness. -- Fergus Henderson [EMAIL PROTECTED] | "I have always known that the pursuit WWW: http://www.cs.mu.oz.au/~fjh | of excellence is a lethal habit" PGP: finger [EMAIL PROTECTED]| -- the last words of T. S. Garp.
Re: Again: Referential Equality
On 27-Jul-1999, Hans Aberg [EMAIL PROTECTED] wrote: I think there is not a big problem with breaking "referential transparency"; the same think happens in pure math often and it is part of a normal procedure of constructing mathematical objects: Referential transparency means that if a = b then F(a) = F(b), where "=" is semantic equality But "=" is in reality just one of several different possible equivalence relations. Sure. But in Mercury, and in mathematics, the way it works is that there is only one equality relation on any given type; there may be many equivalence relations, but one of them is distinguished. If you want to consider values with a different equivalence relation for their equality, then you construct a new type. In mathematics people are generally pretty sloppy about declaring the types, instead assuming that the reader will infer the types from the context, so this may not be so clear in mathematics as it is in Mercury or Haskell. But nevertheless knowing the type (and hence knowing which equivalence relation is being used for equality) is crucial to understanding the mathematics. In Haskell, things are not quite as nice, semantically speaking, as they are in Mercury and mathematics, because Haskell has two different distinguished equivalence relations: `=' and `=='. When you construct a new type, Haskell doesn't let you define equality (`=') for that type, it only lets you define `=='. Haskell promises (and compilers may rely on) referential transparency with respect to `=', but not referential transparency with respect to `=='. Take an example: construct say the real numbers R as the Cauchy sequences of rational numbers Q modulo the equivalence relation that two sequences have the same limit (omitting boring mathematical details). Then a lot of different Cauchy sequences of rational numbers will represent the same real number. (So this corresponds roughly to different references of the same semantic object in a computer language.) These reference have different types: one is the type of real numbers, the other is the type of Cauchy sequences of rationale numbers. So long as the type system keeps the distinction between a type and its representation, constructing new types in this way doesn't break referential transparency. So I think one should not bother too much about breaking referential transparency when allowing access to the underlying runtime covers. On the contrary, it seems that this exactly what one should expect to happen. When you break open the underlying runtime covers (cross an abstraction boundary) what you get is nondeterminism. But there's no reason why this should be or needs to be done in a way that breaks referential transparency. This comment applies as much to mathematics as to Haskell. In mathematics, `x = y = f(x) = f(y)' is an axiom, and so if you define a function which violates this axiom, you have an inconsistent system. If you want your mathematics to be based on sound foundations, then you need to keep track of the types, so that you can avoid such inconsistencies. -- Fergus Henderson [EMAIL PROTECTED] | "I have always known that the pursuit WWW: http://www.cs.mu.oz.au/~fjh | of excellence is a lethal habit" PGP: finger [EMAIL PROTECTED]| -- the last words of T. S. Garp.
RE: Again: Referential Equality
Fergus wrote: On 27-Jul-1999, Simon Marlow [EMAIL PROTECTED] wrote: I would like to have a comparison instruction that compares the internal reference of two objects. Let's call it "req". req :: a - a - Bool By coincidence, I was just looking at GHC's documentation on stable names and pointers, and it seems relevant here. [...] Something like this might do the job for you: req a b = unsafePerformIO $ do a' - makeStableName a b' - makeStableName b return (a' == b') That's exactly what to use in a situation like this. I disagree. `makeStableName' may be the right thing to use, but the above code is not quite the right way of using it. Instead the call to unsafePerformIO should be propagated outwards -- see my other post. Your point is well taken, but he was after all asking for an req with an unsound type. Caveat user. ... if you intend to encapsulate your use of pointer equality in a "safe" abstraction, say a memo table, then use of unsafePerformIO is entirely justified. The req function above is of course an "unsafe" abstraction, because it exposes the representation of a and b. Yes, the use of `unsafePerformIO' is justified in such cases. But the call to `unsafePerformIO' should be from the code defining the safe abstraction. If you put the call to `unsafePerformIO' in an unsafe primitive such as `req', then when your code is compiled with some optimizing compiler which assumes that functions are referentially transparent the resulting executable may dump core. Dump core? I would expect the compiler to disable any such optimizations when it sees an unsafePerformIO. What does GHC do? --FC
Re: Again: Referential Equality
On 27-Jul-1999, Theo Norvell [EMAIL PROTECTED] wrote: On Tue, 27 Jul 1999, Andreas C. Doering wrote: let x=[1..] in x==x would not terminate in the first case but succeed in the second. But, much worse let x = (a,b) in x `req` x = True but (a,b) `req` (a,b) = False So referential transparency is lost. This is a high price to pay. You are right that *something* is needed; but I don't yet know what. One solution is nondeterminism. Yes. But we know how to model nondeterminism in a referentially transparent manner in a pure functional language such as Haskell. There's no need to resort to extensions that break referential transparency if all you want is nondeterminism. -- Fergus Henderson [EMAIL PROTECTED] | "I have always known that the pursuit WWW: http://www.cs.mu.oz.au/~fjh | of excellence is a lethal habit" PGP: finger [EMAIL PROTECTED]| -- the last words of T. S. Garp.
Re: Again: Referential Equality
On 27-Jul-1999, Simon Marlow [EMAIL PROTECTED] wrote: I would like to have a comparison instruction that compares the internal reference of two objects. Let's call it "req". req :: a - a - Bool By coincidence, I was just looking at GHC's documentation on stable names and pointers, and it seems relevant here. [...] Something like this might do the job for you: req a b = unsafePerformIO $ do a' - makeStableName a b' - makeStableName b return (a' == b') That's exactly what to use in a situation like this. I disagree. `makeStableName' may be the right thing to use, but the above code is not quite the right way of using it. Instead the call to unsafePerformIO should be propagated outwards -- see my other post. ... if you intend to encapsulate your use of pointer equality in a "safe" abstraction, say a memo table, then use of unsafePerformIO is entirely justified. The req function above is of course an "unsafe" abstraction, because it exposes the representation of a and b. Yes, the use of `unsafePerformIO' is justified in such cases. But the call to `unsafePerformIO' should be from the code defining the safe abstraction. If you put the call to `unsafePerformIO' in an unsafe primitive such as `req', then when your code is compiled with some optimizing compiler which assumes that functions are referentially transparent the resulting executable may dump core. -- Fergus Henderson [EMAIL PROTECTED] | "I have always known that the pursuit WWW: http://www.cs.mu.oz.au/~fjh | of excellence is a lethal habit" PGP: finger [EMAIL PROTECTED]| -- the last words of T. S. Garp.
Re: Again: Referential Equality
Fergus Henderson wrote: equal x y = unsafePerformIO $ do ptrEq - ptrEqual x y return (ptrEq || deep_equals x y) Note that unlike `req', `equal' here _is_ referentially transparent. No, it's not. If x and y are both bottom you can get unexpected results, i.e., sometimes it terminates, sometimes it doesn't. -- -- Lennart
Re: Again: Referential Equality
At 14:02 +0100 1999/07/28, D. Tweed wrote: As for a math description of references, one could take the view that one always constructs objects a, with references r. Then what is indicated in the language is often the object pairs (a, r) modulo the equivalence relation that the references differ. I'm not sure this is a useful view to take given Lennart Fergus's responses to my previous post saying that the actual references corresponding to named values in a compiled program can fluctuate over the course of program evaluation for various reasons. (I must admit I was surprised that this happens but I guess that's because the FL implementations in textbooks aren't that close to Power-User Haskell Systems(TM) like ghc hbc :-) ) If this is a problem, one should create a type of reference that is stable during the processes. A "reference" need not be something specific, such as a computer address, but could be viewed as method that can be used to address the object. So say object (v1, a1) is copied over to object (v2, a2), where v1 = v2 are the values and a1, a2 are the addresses. In order to make a stable reference, one needs to create an object r which first points at a1 and then at a2. Thus (v1, r) is altered into (v2, r), which in reality will be viewed as identical, having the same reference. The requirement of such a structure will surely affect the implementation of compilers. Now I know this I think just throwing the stuff into a monad of some sort to indicate the non-determinism is as good a solution as any. So I just wanted to give a logical description resolving this referential transparency paradox. How one then chooses to wrap it up in a language is another matter; it should then just be something that is convenient to the user. Hans Aberg * Email: Hans Aberg mailto:[EMAIL PROTECTED] * Home Page: http://www.matematik.su.se/~haberg/ * AMS member listing: http://www.ams.org/cml/
Re: Again: Referential Equality
Frank A. Christoph [EMAIL PROTECTED] wrote: Fergus wrote: If you put the call to `unsafePerformIO' in an unsafe primitive such as `req', then when your code is compiled with some optimizing compiler which assumes that functions are referentially transparent the resulting executable may dump core. Dump core? Unlikely in practice, but possible, yes. I would expect the compiler to disable any such optimizations when it sees an unsafePerformIO. But it might not see the `unsafePerformIO' at the time it was performing the optimization in question; it might just see a couple of calls to `req'. -- Fergus Henderson [EMAIL PROTECTED] | "I have always known that the pursuit WWW: http://www.cs.mu.oz.au/~fjh | of excellence is a lethal habit" PGP: finger [EMAIL PROTECTED]| -- the last words of T. S. Garp.
Re: Again: Referential Equality
On Wed, 28 Jul 1999, Hans Aberg wrote: At 14:02 +0100 1999/07/28, D. Tweed wrote: As for a math description of references, one could take the view that one always constructs objects a, with references r. Then what is indicated in the language is often the object pairs (a, r) modulo the equivalence relation that the references differ. I'm not sure this is a useful view to take given Lennart Fergus's responses to my previous post saying that the actual references corresponding to named values in a compiled program can fluctuate over the course of program evaluation for various reasons. (I must admit I was surprised that this happens but I guess that's because the FL implementations in textbooks aren't that close to Power-User Haskell Systems(TM) like ghc hbc :-) ) If this is a problem, one should create a type of reference that is stable during the processes. A "reference" need not be something specific, such as a computer address, but could be viewed as method that can be used to address the object. I think I misinterpreted what you originally wrote. I'd thought that you were trying to produce an `explanatory theory' explaining what would be happening if the original req idea (comparing internal representations) were to be implemented; I see now that you were describing how you could implement `language defined references' with semantics which mean that the problems that were pointed out don't happen. Clearly with the new proposal assigning references at once for all at creation time is by construction an ok model. ___cheers,_dave__ email: [EMAIL PROTECTED] "He'd stay up all night inventing an www.cs.bris.ac.uk/~tweed/pi.htm alarm clock to ensure he woke early work tel: (0117) 954-5253 the next morning"-- Terry Pratchett
Re: Again: Referential Equality
Fergus Henderson wrote: I'm not sure off-hand what the best fix would be. One possible solution would be to force evaluation of the arguments if they are equal: equal x y = unsafePerformIO $ do ptrEq - ptrEqual x y return (if ptrEq then x `hyperseq` True else deep_equals x y) However, this compromises the nice O(1) performance in that case. Another possible fix would be to rename `equal' as `unsafe_equal', noting that it is referentially transparent so long as neither of its arguments contains bottom or any exceptional value; it would then be the programmer's responsibility to check that all callers ensure that this condition is satisfied for all calls to `unsafe_equal'. The second fix is probably best. But it's still rather ugly. Once opon a time (ca. 1986) I almost implemented a scheme which would use pointer equality in a safe way. The idea is to have each node in the heap tagged if it is fully evaluated or not. So if pointer equality says `equal' and the node is tagged as fully evaluated we can safely use the result, otherwise not. But after considering it for a while, I decided that it would incur bigger runtime costs than the savings for comparisons. AFAIK, it's not been tried yet. Maybe nowadays we could get help from the type system in deciding if a value can be bottom or not (well, I know we can, but again I don't think it's been tried in practice). ... This is OK in Mercury because in Mercury although the operational semantics is required to be sound w.r.t. the declarative semantics, it is not required to be complete; in cases where the declarative semantics says that the result is `yes', it may still be acceptable for the implementation to throw an exception rather than computing the result `yes'. In Mercury, if you want to reason about whether your program will terminate or throw exceptions, you need to use the operational semantics rather than the declarative semantics. Well, given that I think I'll stick to functional languages. ;-) -- -- Lennart
Re: Again: Referential Equality
Lennart Augustsson wrote: ... This is OK in Mercury because in Mercury ... Well, given that I think I'll stick to functional languages. ;-) I appreciate your ;-) Indeed, for lots of logic programmers, Mercury is a functional language in a logic syntax disguise. You can be a functional programmer in heart and kidneys (as the flemmish expression goes) and still stick to Mercury. Bart Demoen
Re: Again: Referential Equality
At 16:49 +0100 1999/07/28, D. Tweed wrote: ... I see now that you were describing how you could implement `language defined references' with semantics which mean that the problems that were pointed out don't happen. Right. I think that in a computer language one tends to think of the semantics as defined via the language, whereas in math one creates a mental image of a semantics (the notions) and then describes it via the notation (or the language). So this possibility of resolve ambiguities by adding a more complete picture to the semantics is often overlooked in computer languages. Then, when the ambiguities have been resolved, one proceeds at finding a better notation. Clearly with the new proposal assigning references at once for all at creation time is by construction an ok model. I am happy to see that my intuition seems to work from the cs point of view. :-) Hans Aberg * Email: Hans Aberg mailto:[EMAIL PROTECTED] * Home Page: http://www.matematik.su.se/~haberg/ * AMS member listing: http://www.ams.org/cml/
RE: Again: Referential Equality
The expression let x=[1..] in x==x would not terminate in the first case but succeed in the second. But, much worse let x = (a,b) in x `req` x = True but (a,b) `req` (a,b) = False So referential transparency is lost. This is a high price to pay. You are right that *something* is needed; but I don't yet know what. Meanwhile Jeff Lewis has a BDD library accessible from Haskell, I believe. [EMAIL PROTECTED] Simon I came up when I tried to implement Binary Decision Diagrams in Haskell some years ago and I have the impression that I need them again soon. It ould be so much nicer with this operation.
RE: Again: Referential Equality
let x=[1..] in x==x would not terminate in the first case but succeed in the second. But, much worse let x = (a,b) in x `req` x = True but (a,b) `req` (a,b) = False So referential transparency is lost. This is a high price to pay. You are right that *something* is needed; but I don't yet know what. I do not think that this is "worse". Such a funtion would have to be used wise. "True" means "Sure both terms are equal, we can save further actions" "False" means "Do not know," It is a primitive which has to be used as in the list comparison. Then, "referential transparency" is recreated, but the termination problem remains. Meanwhile Jeff Lewis has a BDD library accessible from Haskell, I believe. [EMAIL PROTECTED] I will ask him. I made a BDD-lib already, but it uses an array to store the nodes, and garbage collection is explicitely programmed on this array requiring reallocation, contents copying and so forth, very ugly. Andreas --- Andreas C. Doering Medizinische Universitaet zu Luebeck Institut fuer Technische Informatik Ratzeburger Allee 160 D-23538 Luebeck Germany Tel.: +49 451 500-3741, Fax: -3687 Email: [EMAIL PROTECTED] Home: http://www.iti.mu-luebeck.de/~doering quiz, papers, VHDL, music "The fear of the LORD is the beginning of ... science" (Proverbs 1.7)
RE: Again: Referential Equality
I would like to have a comparison instruction that compares the internal reference of two objects. Let's call it "req". req :: a - a - Bool By coincidence, I was just looking at GHC's documentation on stable names and pointers, and it seems relevant here. http://research.microsoft.com/users/t-simonm/ghc/Docs/latest/l ibraries/libs- 14.html Something like this might do the job for you: req a b = unsafePerformIO $ do a' - makeStableName a b' - makeStableName b return (a' == b') That's exactly what to use in a situation like this. Pointer equality loses referential transparency in general (as Simon P.J. pointed out), hence the use of the I/O monad in our Stable Name API. Furthermore, if you intend to encapsulate your use of pointer equality in a "safe" abstraction, say a memo table, then use of unsafePerformIO is entirely justified. The req function above is of course an "unsafe" abstraction, because it exposes the representation of a and b. Cheers, Simon
RE: Again: Referential Equality
I would like to have a comparison instruction that compares the internal reference of two objects. Let's call it "req". req :: a - a - Bool By coincidence, I was just looking at GHC's documentation on stable names and pointers, and it seems relevant here. http://research.microsoft.com/users/t-simonm/ghc/Docs/latest/libraries/libs- 14.html Something like this might do the job for you: req a b = unsafePerformIO $ do a' - makeStableName a b' - makeStableName b return (a' == b') --FC
Re: Again: Referential Equality
Andreas C. Doering wrote: | I would like to have a comparison instruction that compares the internal | reference of two objects. It might be of interest here to talk about a paper that Dave Sands and I have recently submitted to a conference, about something we call "observable sharing". It talks about an extension to Haskell that we made in order to describe hardware circuits in Haskell in a convenient way. So we present a different solution to the problem that O'Donnel describes in [1]. The contructs we add to the language are: type Ref a = ... ref :: a - Ref a deref :: Ref a - a (=) :: Ref a - Ref a - Bool This basically gives you ML-style but non-updatable references, but you can compare them for equality. You can also see it as pointer equality, but only on objects of a certain type, so that you have to explicit at creation time if you want to pointer-compare them later. let x = ref 27 in x = x yields True, whereas ref 27 = ref 27 yields False. So, it does break referential transparency. But, in the paper, we show that very many transformations that a compiler may safely perform in normal Haskell can still be performed in Haskell with the extension. In fact, *all* the laws from Moran's and Sand's paper about the Lazy Improvement Theory [2] still hold in Haskell with the Ref extensions! If you want a (draft) copy of the paper, let me know. Regards, Koen. References: [1] O'Donnell, J., Generating netlists from executable circuit specifications in a pure functional language, Functional Programming Glasgow, 1993. [2] Moran, A. and Sands, D., Improvement in a Lazy Context: An Operational Theory for Call-By-Need, POPL '99, 1999. -- Koen Claessen http://www.cs.chalmers.se/~koen phone:+46-31-772 5424 e-mail:[EMAIL PROTECTED] - Chalmers University of Technology, Gothenburg, Sweden
Re: Again: Referential Equality
"D. Tweed" wrote: On Tue, 27 Jul 1999, Simon Marlow wrote: req a b = unsafePerformIO $ do a' - makeStableName a b' - makeStableName b return (a' == b') That's exactly what to use in a situation like this. Pointer equality loses referential transparency in general (as Simon P.J. pointed out), hence the use of the I/O monad in our Stable Name API. Furthermore, if you intend to encapsulate your use of pointer equality in a "safe" abstraction, say a memo table, then use of unsafePerformIO is entirely justified. The req function above is of course an "unsafe" abstraction, because it exposes the representation of a and b. Just an idle curiousity question: when you say it loses referential transparency am I right in saying it this is only with respect to compile time transformations ( program proofs,etc) but that there's no problem _for a given compiled program_ about req a b changing it's value depending upon the way demand drives the lazy evaluation reduction strategy, or is there a subtlety there? A particular call to `req' may change from True to False or vice versa between different runs of the program. Just imagine a parallel implementation that does things "behind your back". And every implementation has one of those! It's called the garbage collector. :-) I know that the hbc garbage collector happily does things that changes the sets of objects that are pointer equal before and after a GC. So I think IO is a good place to put it. If Haskell had a Nondeterministic monad then that would be the place. -- -- Lennart
RE: Again: Referential Equality
On Tue, 27 Jul 1999, Andreas C. Doering wrote: let x=[1..] in x==x would not terminate in the first case but succeed in the second. But, much worse let x = (a,b) in x `req` x = True but (a,b) `req` (a,b) = False So referential transparency is lost. This is a high price to pay. You are right that *something* is needed; but I don't yet know what. One solution is nondeterminism. req x y is False when x and y are not 'equal' req x y is True | False when x and y are 'equal' where 'equal' means the same as the built-in == operator for the type, or structural equality for user-defined types and where a | b means a nondeterministic choice between a and b. Now let x=[1..] in x == x can not be proved to terminate with Andreas's optimized definition of List == (although it also can not be proved not to terminate). It is valid to optimize (a,b) `req` (a,b) to let x = (a,b) in x `req` x . However, the inverse transformation increases nondeterminism and thus would not be valid. So if you define referential transparency as the saying that E[ x / F] and let x = F in E are equivalent, then referential transparency is still 'lost'. But when nondeterminism is involved, this equivalence is usually already an inequivalence. In 'good' implementations, there would be a pragmatic understanding that req x y will be True when x and y are the same reference. Cheers, Theo Dr. Theodore Norvell, Assistant Professor [EMAIL PROTECTED] Memorial University of Newfoundlandhttp://www.engr.mun.ca/~theo Vox: (709) 737-8962 Fax: (709) 737-4042
RE: Again: Referential Equality
On Tue, 27 Jul 1999, Simon Marlow wrote: req a b = unsafePerformIO $ do a' - makeStableName a b' - makeStableName b return (a' == b') That's exactly what to use in a situation like this. Pointer equality loses referential transparency in general (as Simon P.J. pointed out), hence the use of the I/O monad in our Stable Name API. Furthermore, if you intend to encapsulate your use of pointer equality in a "safe" abstraction, say a memo table, then use of unsafePerformIO is entirely justified. The req function above is of course an "unsafe" abstraction, because it exposes the representation of a and b. Just an idle curiousity question: when you say it loses referential transparency am I right in saying it this is only with respect to compile time transformations ( program proofs,etc) but that there's no problem _for a given compiled program_ about req a b changing it's value depending upon the way demand drives the lazy evaluation reduction strategy, or is there a subtlety there? (I'm just curious about the use of the IO monad, which regulates things which depend on the an underlying state which may change with time in a difficult to predict way depending on the precise pattern of reduction, rather than say a `compile time monad'.) ___cheers,_dave__ email: [EMAIL PROTECTED] "He'd stay up all night inventing an www.cs.bris.ac.uk/~tweed/pi.htm alarm clock to ensure he woke early work tel: (0117) 954-5253 the next morning"-- Terry Pratchett
