4 ms·

Patch theory?

• deleted 11y ago
  [deleted]
• mafribe 11y ago
  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.pdf https://ifl2014.github.io/submissions/ifl2014_submission_32....
  • 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 ago
      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.
      • coolsunglasses 11y ago
        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.