Type systems typically allow reasoning about the shape of data structures, and of functions that consume/produce them. Has anyone seen any type systems / theories for describing the shape and compatibility of changes (patches) to data structures? You could use this to reason about whether two operations on a data structure could be reordered, for example. You could also use it to reason about replicated state.

Types might contain much more information than the shape of data for sure. Have you checked Agda/Idris/ Dependent Types/Proof checkers? Types can express many kind of "relations" in the logic of the underlying code it is used with/in.

This is something I’m super interested in too. I don’t think I’ve seen it much in type theory tbh, and I think it’s super important. I’ve seen https://www.movereem.nl/files/2017SANER-eventsourcing.pdf, which kind of hints at there being some ‘algebra’ or something of changes to event streams. Swift’s ABI stability stuff might also be interesting too: https://forums.swift.org/t/swift-org-blog-abi-stability-and-more/20250

Thanks for the links. Regarding the type theory, I've found several papers on "patch theories" which formalise patches to code repositories, and some authors (https://bit.ly/2lRgj6S) have suggested that we can generalise our thinking about code to include replicated state (and therefore local state, which is strictly simpler). I've not really dug into this yet though.

I'm really interested in this too, specifically typed database migrations

@Nick Smith I'm familiar with some work in this area. I've been working on a type system for a language called Datafun (http://www.rntz.net/datafun) which enforces monotonicity, and monotonicity turns out to be related to eventual consistency in distributed and concurrent systems (see http://bloom-lang.net/calm/ and Lindsey Kuper's work on LVars). The idea is to only permit increasing changes, so the ordering on a type describes how things of that type may change. Kevin Clancy, Heather Miller, & al. have applied a similar type system to distributed programming with CRDTs (https://infoscience.epfl.ch/record/231867/files/monotonicity-types.pdf). Along slightly different lines, there's a lot of work in incremental computation, which implicitly has some notion of change underlying it. The most popular work here is in FRP systems or in self-adjusting computation (eg. the Incremental library for OCaml). However, the work I'm most familiar with, and which makes the notion of changes as a data type of their own explicit, is the incremental λ-calculus (https://www.informatik.uni-marburg.de/~pgiarrusso/ILC/ and https://www.informatik.uni-marburg.de/~pgiarrusso/papers/pldi14-ilc-author-final.pdf). I've adapted this approach to handle Datafun's type system, but this isn't published in its entirety yet (sometime in the next year). However, neither of these (yet!) explicitly accounts for reasoning about when changes can/can't be reordered. (In the case of CRDTs, the whole point is that changes can always be reordered, which is a handy property but can require a lot of cleverness to achieve.)

@rntz Thanks for these links! I'm going to look into them, though I'm definitely looking for a type system that can deal with composition and reordering of changes. One use case I have in mind is making it impossible to express false dependencies between parts of a program. For example, instead of having the type signature of a state transition function inferred as

state -> state

, I'd like to see it be given a type signature

state -> delta state

, where the result value can only be consumed by other functions that (may) need to read from the subset of state that was changed (else you'd get a type error about a "false dependency", or the IDE would just rearrange the code to remove the false dependency). I need a type system that will let me test out this experience. Worst case, I'll have to become a type theorist and just invent it!