3 ms·
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?
by coolsunglasses 11y ago
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?
- mafribe 11y agoI 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.
- coolsunglasses 11y agoIt 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.