Re: DDC compiler and effects; better than Haskell? (was Re: [Haskell-cafe] unsafeDestructiveAssign?)

My intuition says the proper formalism is that undo is left adjoint to redo. They together form a monad in the category of redoable actions. return lifts doable actions to undoable ones by attaching an empty undo stack. join lowers (reflects) a first-class undoable action out of the undo stack and makes it doable. The reason that the adjunction view is more fundamental here is that the monad is in some sense the equivalence class of all observationally equivalent undo/redo pairs. That is, undo need not actually restore the previous state: it is sufficient to restore any action that, when redone, gives the same state as the one before undo. There may be justification for this idea in Rossiter et al, "Process as a World Transaction" (http://computing.unn.ac.uk/staff/CGNR1/anpa064.pdf), though I haven't had time to read it yet. Dan Peter Verswyvelen wrote:

I think version is control is really just a subset of a larger effect theory. E.g. I've been experimenting with a parallel undo/redo system in C#, where some actions can commute and be undone separately, and for detecting this, the actions need to explicitly expose what they will change; so this also seems in the same line of research (and has been reported earlier in the thread "darcs as undo/redo system").

And if I recall correctly, imperative compilers can reorder and parallelize instructions based on what they read/write; again this feels the same.

Like John said, it will be interesting when the operating system itself exposes all dependencies (what it reads/writes), so that if e.g. content of file A is used to generate content of file B, that this is not some spooky action at a distance. Now the OS is treated like a big black IO box (realworld in -> realworld out), just because we're still stuck with dumb hierarchical file systems and other opaque IO.

Another example might be FRP / Yampa, and the recent work of Hai (Paul) Liu, Paul Hudak and co, where causal commutative arrows are invented. AFRP computations really commute, while standard arrows are just a generalization of monads, so not really suitable for capturing the parallel nature of AFRP. The way I discovered this myself, is that when you have e.g. a large tree of user interface widgets, represented by a big arrow circuit, and the user edits just the one widget in one branch (which happens when e.g. the mouse is captured), then with the current arrows system all branches will be visited depth first. But of course only the path towards the widget that will change needs to be visited, all the other remain constant.

Since I don't have any academic backgrounds - only intuition - I'm not sure if these topics are related, but they sure feel like it :-)

On Fri, Aug 14, 2009 at 11:38 PM, Jason Dagit wrote:

...

...

Hmmm, my point (perhaps I wasn't clear), is that different effects have different commutability properties. In the case of a file system, you can commute two sequential reads from two different files. This has no effect on the result of the computation, assuming no interference from other programs -- and if there _is_ interference from other programs, then guarantees go out the window, _with or without_ commuting. Monads are an insufficient structure to capture the fine semantics of effects. Something more powerful is needed. And in general, the way effects combine and commute is quite complicated and needs to be baked into the effect system, rather than being the responsibility of a lowly developer. It's really interesting. This is related to the reasoning darcs does with

On Fri, Aug 14, 2009 at 1:41 PM, John A. De Goes wrote: patches (aka patch theory). Patches tend to have effects on your repository. Sometimes those effects can be reordered without changing the final state of the repository. Other times, it is not possible to reorder them without either having a non-sensible final state or different final states. I've never thought about reading research about effect systems for the sake of version control. I'll have to look into this.

Jason

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe