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