David-Sarah Hopwood wrote: > Mark S. Miller wrote: >> On Tue, Dec 8, 2009 at 8:47 AM, <[email protected]> wrote: >>> Thank you for the writeup; interesting. Just one point of motivation >>> that perhaps I missed from the original post: >>> >>> On Mon, Dec 7, 2009 at 11:17 PM, David-Sarah Hopwood >>> <[email protected]> wrote: >>>> To dodge this issue, let's provisionally call a function *instance* >>>> "copacetic" [*] if: >>>> - that instance has only captured copacetic values, and >>>> - it has no side effects and is deterministic whenever it is >>>> only called with copacetic argument values, and >>>> - it uses no side-effecting or nondeterministic primitives. >>> I'm getting at something similar but distinct, call it "i-copacetic". >>> :) Specifically: >>> >>> - it has no side effects on its lexical environment regardless >>> of its argument values >>> >>> The motivation is this: An object's state is managed by some >>> surrounding system. However, it is allowed to expose "read()" services >>> to the outside world that do not participate in this state management. >>> Each "read()" service may side-effect the supplied arguments, but it >>> must not side-effect the lexical environment of the service (i.e., the >>> object itself). >> How is this different from E's DeepFrozen or Joe-E's Immutable? > > Since E has no nondeterministic ambient operations, DeepFrozen in E > implies determinism for calls with only DeepFrozen arguments. But in > general, if a language does have nondeterministic primitives (say, > nondeterministic floating point arithmetic), then a copacetic function > would be verified to be implemented in a deterministic sublanguage. > In that case, DeepFrozen would differ from (copacetic without the > argument and result checks).
Actually, DeepFrozen necessarily implies non-access to nondeterminism, since otherwise a "DeepFrozen" value could be observed to change. So DeepFrozen is the same as (copacetic without the argument and result checks) -- or at least to what I intended that to mean, despite some imprecision in the definition. -- David-Sarah Hopwood ⚥ http://davidsarah.livejournal.com
signature.asc
Description: OpenPGP digital signature
