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".
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.
Comments
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.