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

[Dan Weston]

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<dagit at codersbase.com> wrote:
>>
>> On Fri, Aug 14, 2009 at 1:41 PM, John A. De Goes <john at n-brain.net> 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
>> 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 at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 
>