Large-scale, well-typed edits in Unison, and reimagining version control | Hacker News Reader

Large-scale, well-typed edits in Unison, and reimagining version control

unisonweb.org

44 pointsdahjelle11 comments

At the first sight, I though it was a new version of https://www.cis.upenn.edu/~bcpierce/unison/ but it seems completely different.

I personally like the (language-dependent) "series of actions" approach.

So, you quite literally send to the VCS "add this parameter with default value <foo> to this function", "make a copy of this function", "add this function", etc. With transactions.

And the VCS "just" replays the edits. Note that the VCS will occasionally have to munge the human-readable names in the case of what would be otherwise a conflict. But the VCS doesn't deal with things at that level anyways. You really should end up dealing with things at the AST level and rebuilding the source code when necessary.

Think of it like a refactoring tool integrated with the VCS.

This is a huge surprise! I had been under the assumption that asynchronous semantic edits were the only true way forward. Synchronous large-scale edits?! If you can make it work, even only half of the time... that is an enormous productivity boost.

Well--fair warning, it's happy hour--but allow me dump my incoherent gut armchair objections.

- Large-scale edits mess with large-scale invariants. Can this edit calculus and scoping mechanism truly deal with arbitrary changes? Or is "arbitrary changes" a white rabbit, and can you come up with a calculus that handles all "reasonable" changes?

- I had previously thought that the only way we're going to get past the {software upgrade,data migration} bottleneck is through semantic VC. Developers make mistakes. Software evolution as a gradient (rather than the status quo of progress in fits-and-starts) seems extremely unsafe. Does Unison make all mistakes undo-able?

- Won't "branchless" conflict-free versioning be the same as constant forking, creating an enormously fragmented software project? (So postmodern!) How do you get everyone back on the same "master" mainline; surely not all possible Edits can commute?

I guess all these concerns are irrelevant if you treat synchronous editing as the golden path, and fall back to async for the hard stuff.

What's semantic VC?

Oh.. version control?

Yeah it's covered halfway through. VCS that does merges wrt code structure rather than lines of text.

Patch theory?

The difference, I think, from patch theory is that Unison always preserves types while editing. Patch theory works with untyped text. The main result of [1], which Unison seems to be based on, is that you can form any well-typed term in the simply typed lambda-calculus this way. Unison seems to go even further: "[f]rom any starting codebase we can get to any other codebase".

[1] Editing Functional Programs Without Breaking Them, Amsden et al. https://ifl2014.github.io/submissions/ifl2014_submission_32....

I wasn't aware patch theory was necessarily limited to untyped text, that's why I brought it up. Do we know where Unison is drawing from for what it does?

I don't think patch theory is untyped in principle. But all developments I've seen are untyped. And it's probably good this way, for typically you don't want to tie a version control system to a specific programming language / typing system. There is recent work on patch theory using category theory [2] and homotopy type theory [3], maybe that introduces a types angle (I have only skimmed these papers).

I think Unison is based on [1] quoted above, but I'm not sure.

[2] S. Mimram, C. Di Giusto, A Categorical Theory of Patches.

[3] C. Angiuli, E. Morehouse, D. R. Licata, R. Harper, Homotopical Patch Theory.

It seems wasteful not to use insights from one domain (untyped, textual) in another (typed, contextual).

I knew about (not that I understand it) the connection homotopy...mostly just worried there's work happening that isn't informed by research.

Reply on news.ycombinator.com