6 ms·

Data evolution with set-theoretic types

127 points by josevalim 2y ago

josevalim 2y ago
Author here. This is probably the article that took me the longest to write, roughly 15 months, and I may still not have explained all concepts with the clarity they deserve and I intended to. If there is any feedback or questions, I'd be glad to answer them!
- practal 2y ago
  Stuff like this is why I don't like type systems. What you want to do is easy, but it becomes difficult to explain in a sane way (15 months difficult), because you need to work around the limitations of type systems. When you say "set-theoretic types", I hear, "get rid of types, just give me logic".
  - ryanschaefer 2y ago
    > what you want to do is easy Easy to implement, hard to get correct. It inverts where you do work in a system. It can be hard to implement robust types but once that’s done it’s easy to know what you are writing is correct.
  - josevalim 2y ago
    The work to develop the base theory, which this article presents, takes 15 months, but it doesn't take 15 months to read it (and hopefully it won't take as long to use it either). Whenever you use a programming language, you may work with data structures that took months to formalize and several more years to optimize, yet no one is saying "throw our data structures away". Even things like pretty printing and formatting a float have collectively several years of research behind them, yet the API is often a single function call. Of course, you can still not like types, and making it harder to evolve libraries over time is a good reason. But using the time it takes to formalize its underlying concepts is not a strong argument against them. The goal is that someone will spend this time, precisely so you don't have to. :)
    - Conscat 2y ago
      I have seen multiple users of one certain popular programming language claim that data structures besides a dynamic length array and a hash table have no useful application.
      - caspper69 2y ago
        They wouldn't also happen to throw out memory safety guarantees one level up by using a ton of array indexing, would they?
      - tadfisher 2y ago
        Clojure? Sounds like something Hickey would say.
    - practal 2y ago
      Oh, I like formalising things, don't get me wrong, and I don't mind spending time on it at all. I just don't like doing it via types, and looking at how much time you spent on what, I rest my case.
  - ddellacosta 2y ago
    > because you need to work around the limitations of type systems. What limitations of type systems are you talking about? > When you say "set-theoretic types", I hear, "get rid of types, just give me logic". A type theory/type system is a logic, so I don't really understand this point. https://en.wikipedia.org/wiki/Type_theory#Logic https://en.wikipedia.org/wiki/Type_theory#Logic
    - practal 2y ago
      Yes, a type theory is a logic, but not a particularly good one. It is limiting to have to under-approximate the mathematical universe via statically typed chunks before being able to talk about the objects in the universe, and the article just describes another instance of why that is problematic in practice. The alternative I propose is simpler than you would think, and definitely simpler than type theory, but it is also very new: http://abstractionlogic.com http://abstractionlogic.com . And of course, it doesn't come with a fixed algorithm for type checking, but going forward and in the age of AI, I think that will turn out to be an advantage.
      - ddellacosta 2y ago
        > Yes, a type theory is a logic, but not a particularly good one. Given the context of the original post, type theory at least has the benefit of actually existing in industrial languages in the form of a bunch of implemented and in-use type systems. > It is limiting to have to under-approximate the mathematical universe via statically typed chunks before being able to talk about the objects in the universe, and the article just describes another instance of why that is problematic in practice. > > The alternative I propose is simpler than you would think, and definitely simpler than type theory, but it is also very new: http://abstractionlogic.com http://abstractionlogic.com . And of course, it doesn't come with a fixed algorithm for type checking, but going forward and in the age of AI, I think that will turn out to be an advantage. That's helpful in understanding where you're coming from, but now I'm even more perplexed--what you've linked to seems extremely theoretical. The closest to something my industrial programmer brain can grasp and read that I'd care about (in the context of the original post we're discussing) is https://obua.com/publications/automating-abstraction-logic/1/ https://obua.com/publications/automating-abstraction-logic/1..., which seems focused on theorem proving. None of this is meant to suggest that I don't see the value in what you've linked to--it will take me some time to absorb, but I will take a closer look--but if you want to come into a discussion about a post like this one and criticize it, and more generally type systems, I think you'd be better off showing more directly how your approach can solve the same problem (or how it doesn't need to solve it, which it sounds like you're implying) in a way that doesn't take reading through a bunch of fairly abstract posts and papers or watching a five-part video series first. And if there's no actual implementation (that I can see at least) then don't expect me, an industrial programmer--like most folks on HN I would guess vs. e.g. lambda-the-ultimate or whatever--to consider it worthwhile past idle curiosity. I see value in Valim's post because it identifies a problem with type systems that I understand and have encountered, and provides an incremental and pragmatic solution to that. It doesn't seem like you're offering a coherent, practical alternative, regardless of the validity of your arguments ("It is limiting to have to under-approximate the mathematical universe via statically typed chunks before being able to talk about the objects in the universe" makes intuitive sense to me in this context, at least).
- ddellacosta 2y ago
  This is great stuff! As a Haskell fan who uses Elixir (and Erlang) in my day job, I'm really looking forward to seeing how we can leverage more of the new set-theoretic type features showing up in Elixir. Revisions seem like something I've never really seen before in any of the type systems I've used, so I'm excited to see how it can be leveraged in a real production system. Thanks for the post.
beders 2y ago
These are great examples of difficulties people will encounter in all popular statically typed languages sooner or later. I find the solution presented interesting but it is limited to the 3 operations mentioned. The alternative to this runtime schema checks and treating your data as data - the data you are working with is coming from an external system and needs to be runtime-validated anyways. Throw in some nil-punting and you can have a very flexible system that is guarded by runtime checks.
- mrkeen 2y ago
  Agreed that it is naive to assume that static types will keep some kind of consistency on the bytes that come in on the wire, but it misses the point. With static types, you do one transformation from bytes to a proper data type at the boundary. The static type information propogates bidirectionally deep into the guts of the system. If you're 10 layers in, and want to invoke getUserId() on an object, you just add it to your type. Now your endpoint can return 400s without you needing to add extra nil-checks somewhere (or multiple places) from layers 1 to 10 (which realistically will turn into 500s).
  - Vampiero 2y ago
    Realistically you can design a runtime-checked interface that uses option types instead of nulls, thereby guaranteeing static correctness and preventing common pitfalls at the cost of making the usage pattern a bit more verbose.
  - delusional 2y ago
    > but it misses the point. I don't think it misses the point as much as it's an entirely different point. When I talk to my coworkers about the uses of these automated marshaling systems at the boundary, they're not talking about correctness or "evolution". They talk about how annoying they find it to type. In the fingers hitting keyboard sense of that word. They explicitly don't want a change 10 layers deep to result in any error in the parsing layer. They want the magical system to just do something at runtime.
- manx 2y ago
Groxx 2y ago
Yea, this is an issue rather near and dear to my heart (due to pain). I very much appreciate strong and safe types, but it tends to mean enormous pain when making small obvious fixes to past mistakes, and you really don't want to block those. It just makes everything harder in the long term. As an up-front caveat for below: I don't know Elixir in detail, so I'm approaching this as a general type/lang-design issue. And this is a bit stream-of-consciousness-y and I'm not really seeking any goal beyond maybe discussion. --- Structural sub-typing with inference (or similar, e.g. perhaps something fancier with dependent types) seems like kinda the only real option, as you need to be able to adapt to whatever bowl of Hyrum Slaw[1] has been created when you weren't looking. Allowing code that is still provably correct to continue to work without modification seems like a natural fit, and for changes I've made it would fairly often mean >90% of users would do absolutely nothing and simply get better safety and better behavior for free. It might even be an ideal end state. I kinda like the ergonomics of `revision 2` here, it's clear what it's doing and can provide tooling hints in a rather important and complicated situation... but tbh I'm just not sure how much this offers vs actual structural typing, e.g. just having an implicit revision per field. With explicit revisions you can bundle interrelated changes (which is quite good, and doing this with types alone ~always requires some annoying ceremony), but it seems like you'll also be forcing code to accept all of v2..N-1 to get the change in vN because they're not independent. The "you must accept all intermediate changes" part is in some ways natural, but you'll also be (potentially) forcing it on your users, and/or writing a lot of transitioning code to avoid constraining them. I'm guessing this is mostly due to Elixir's type system, and explicit versions are a pragmatic tradeoff? A linear rather than combinatoric growth of generated types? >It is unlikely - or shall we say, not advisable to - for a given application to depend on several revisions over a long period of time. They are meant to be transitory. An application, yes - applications should migrate when they are able, and because they are usage-leaf-nodes they can do that without backwards compatibility concerns. But any library that uses other libraries generally benefits from supporting as many versions as possible, to constrain the parent-library's users as little as possible. It's exactly the same situation as you see in normal SAT-like dependency management: applications should pin versions for stability, libraries should try to allow as broad of a range as possible to avoid conflicts. >Would downcasting actually be useful in practice? That is yet to be seen. I would pretty-strongly assume both "yes" and "it's complicated". For end-users directly touching those fields: yes absolutely, pick your level of risk and live with it! This kind of thing is great for isolated workarounds and "trust me, it's fine" scenarios, code has varying risk/goals and that's good. Those happen all the time, even if nobody really likes them afterward. But if those choices apply to all libraries using it in a project... well then it gets complicated. Unless you know how all of them use it, and they all agree, you can't safely make that decision. Ruby has refinements which can at least somewhat deal with this, by restricting when those decisions apply, and Lisps with continuations have another kind of tool, but most popular languages do not... and I have no idea how possible either would be in Elixir. --- All that probably summarizes as: if we could boil the ocean, would this be meaningfully different than structural typing with type inference, and no versioning? It sounds like this might be a reasonable middle-ground for Elixir, but what about in general, when trying to apply this strategy to other languages? And viewed through that lens, are there other structural typing tools worth looking at? [1] https://en.wiktionary.org/wiki/Hyrum%27s_law https://en.wiktionary.org/wiki/Hyrum%27s_law
Moosieus 2y ago
This is some interesting shit, I love it! At least that parts I think I understand :P > The goal of data versioning is to provide more mechanisms for library authors to evolve their schemas without imposing breaking changes often. Application developers will have limited use of this feature, as they would rather update their existing codebases and their types right away. Although this may find use cases around durable data and distributed systems. "Hard cutover" is definitely a lot less laborious, but often times incremental updates are necessary - large teams, existing tables and whatnot. To that end, I would foresee a lot of appeal in app dev when applied to database migrations.
harrisi 2y ago
Some initial concerns when thinking about this: - Understanding how it expands the surface area of both the API and discussion of a struct (and thus also libraries and dependencies of the librar{y,ies}). Now you don't need to ask someone if they're using v1.0 of some package, but also which revision of a struct they're using, which they may not even know. This compounds when a library releases a new breaking major version, presumably - `%SomeStruct{}` for v2 may be different from `%SomeStruct{}` v1r2. - Documentation seems like it would be more complex, as well. If `%SomeStruct{}` in v1.0 has some shape, and you publish `v1.1`, then realize you want to update the revision of `%SomeStruct{}` with a modified (or added) field, would there be docs for `v1.1` and `v1.1r2`? or would `v1.1` docs be retroactively modified to include `%SomeStruct{}v1.1r2`? - The first example is a common situation, where an author realizes after it's too late that the representation of some data isn't ideal, or maybe even isn't sufficient. Typically, this is a solved with a single change, or rarely in a couple or few changes. I'm not sure if the complexity is worth it. I understand the desire to not fragment users due to breaking changes, but I'm not sure if this is the appropriate solution. - How does this interact with (de-)serialization? I happen to be working with the SQLite file format currently, and I generally really enjoy data formats. It's not exactly the same as this, since runtime data structures are ephemeral technically, but in reality they are not. The typical strategy for any blob format is to hoard a reasonable amount of extra space for when you realize you made a mistake. This is usually fine, since previous readers and writers ought to ignore any extra data in reserved space. One of the things one quickly realizes when working with various blob formats is the header usually has (as a guess), 25% of it allocated to reserved space. However, looking at many data formats over the last several decades, it's extraordinarily rare to ever see an update to them that uses it. Maybe once or twice, but it's not common. One solution is to have more variable-length data, but this has its own problems. So, in general, I'm very interested in this problem (which is a real problem!), and I'm also skeptical of this solution. I am very willing to explore these ideas though, because they're an interesting approach that don't have prior art to look at, as far as I know. EDIT: Also, thanks for all the work to everyone on the type system! I'm a huge fan of it!
- harrisi 2y ago
  I forgot to mention, the typical situation for these things for added elements is to add `_ex` or the like, which is not a great solution. You can see this in various places in Erlang, especially around erl_interface and related aspects. On the flip side, what if you realize a data structure needs to remove elements? Say revision 2 adds a field, but revision 3 removes it?
airstrike 2y ago
That was an interesting read. Thanks for sharing and congrats on getting it out there. Two bits stood out and made me think, somewhat in disagreement: > If “data_schema” changes a user facing type, such as the Schema type above, in a backwards incompatible manner, its authors have to release a new major version. A new major version can be a fork on the road. Libraries that depend on “data_schema”‘s new version won’t accept the old ones. Old libraries that depend on “data_schema” have to be updated and potentially forced to also release a new major version, cascading the problem. If any package along the way is unmaintained, it can stall and complicate further downstream updates. I wouldn't call it a fork on the road. More like growing pains. This is to be expected of any dependency you have, and it's on you to keep your own code up-to-date. If the original Schema was indeed incorrect, it warrants fixing, even if it's an edge case. And then > In our v1 of Schema, we allowed name to only be a string(). In a statically typed language, we are effectively proving that all uses of Schema has a string() name. When we allow the name to also be nil in v2, that should not introduce bugs in our software yet because, by definition, there is no instance of Schema where the name is nil! > In other words, all existing code remains correct, but most type systems would immediately flag them as wrong, on the possibility they may receive a nil value. There must be a better way and that’s what we study in this article. Personally I don't think that what is proposed here is strictly better. I'd rather have to explicitly change my code to match the new shape of the Schema than to have it magically work. If I don't make changes now, I'm just punting that complexity for later and it's going to come back to bite me in some other issue that will be twice as hard to debug.

127 points by josevalim 2y ago

Author here. This is probably the article that took me the longest to write, roughly 15 months, and I may still not have explained all concepts with the clarity they deserve and I intended to. If there is any feedback or questions, I'd be glad to answer them!

practal 2y ago
Stuff like this is why I don't like type systems. What you want to do is easy, but it becomes difficult to explain in a sane way (15 months difficult), because you need to work around the limitations of type systems. When you say "set-theoretic types", I hear, "get rid of types, just give me logic".
- ryanschaefer 2y ago
  > what you want to do is easy Easy to implement, hard to get correct. It inverts where you do work in a system. It can be hard to implement robust types but once that’s done it’s easy to know what you are writing is correct.
- josevalim 2y ago
  The work to develop the base theory, which this article presents, takes 15 months, but it doesn't take 15 months to read it (and hopefully it won't take as long to use it either). Whenever you use a programming language, you may work with data structures that took months to formalize and several more years to optimize, yet no one is saying "throw our data structures away". Even things like pretty printing and formatting a float have collectively several years of research behind them, yet the API is often a single function call. Of course, you can still not like types, and making it harder to evolve libraries over time is a good reason. But using the time it takes to formalize its underlying concepts is not a strong argument against them. The goal is that someone will spend this time, precisely so you don't have to. :)
  - Conscat 2y ago
    I have seen multiple users of one certain popular programming language claim that data structures besides a dynamic length array and a hash table have no useful application.
    - caspper69 2y ago
      They wouldn't also happen to throw out memory safety guarantees one level up by using a ton of array indexing, would they?
    - tadfisher 2y ago
      Clojure? Sounds like something Hickey would say.
  - practal 2y ago
    Oh, I like formalising things, don't get me wrong, and I don't mind spending time on it at all. I just don't like doing it via types, and looking at how much time you spent on what, I rest my case.
- ddellacosta 2y ago
  > because you need to work around the limitations of type systems. What limitations of type systems are you talking about? > When you say "set-theoretic types", I hear, "get rid of types, just give me logic". A type theory/type system is a logic, so I don't really understand this point. https://en.wikipedia.org/wiki/Type_theory#Logic https://en.wikipedia.org/wiki/Type_theory#Logic
  - practal 2y ago
    Yes, a type theory is a logic, but not a particularly good one. It is limiting to have to under-approximate the mathematical universe via statically typed chunks before being able to talk about the objects in the universe, and the article just describes another instance of why that is problematic in practice. The alternative I propose is simpler than you would think, and definitely simpler than type theory, but it is also very new: http://abstractionlogic.com http://abstractionlogic.com . And of course, it doesn't come with a fixed algorithm for type checking, but going forward and in the age of AI, I think that will turn out to be an advantage.
    - ddellacosta 2y ago
      > Yes, a type theory is a logic, but not a particularly good one. Given the context of the original post, type theory at least has the benefit of actually existing in industrial languages in the form of a bunch of implemented and in-use type systems. > It is limiting to have to under-approximate the mathematical universe via statically typed chunks before being able to talk about the objects in the universe, and the article just describes another instance of why that is problematic in practice. > > The alternative I propose is simpler than you would think, and definitely simpler than type theory, but it is also very new: http://abstractionlogic.com http://abstractionlogic.com . And of course, it doesn't come with a fixed algorithm for type checking, but going forward and in the age of AI, I think that will turn out to be an advantage. That's helpful in understanding where you're coming from, but now I'm even more perplexed--what you've linked to seems extremely theoretical. The closest to something my industrial programmer brain can grasp and read that I'd care about (in the context of the original post we're discussing) is https://obua.com/publications/automating-abstraction-logic/1/ https://obua.com/publications/automating-abstraction-logic/1..., which seems focused on theorem proving. None of this is meant to suggest that I don't see the value in what you've linked to--it will take me some time to absorb, but I will take a closer look--but if you want to come into a discussion about a post like this one and criticize it, and more generally type systems, I think you'd be better off showing more directly how your approach can solve the same problem (or how it doesn't need to solve it, which it sounds like you're implying) in a way that doesn't take reading through a bunch of fairly abstract posts and papers or watching a five-part video series first. And if there's no actual implementation (that I can see at least) then don't expect me, an industrial programmer--like most folks on HN I would guess vs. e.g. lambda-the-ultimate or whatever--to consider it worthwhile past idle curiosity. I see value in Valim's post because it identifies a problem with type systems that I understand and have encountered, and provides an incremental and pragmatic solution to that. It doesn't seem like you're offering a coherent, practical alternative, regardless of the validity of your arguments ("It is limiting to have to under-approximate the mathematical universe via statically typed chunks before being able to talk about the objects in the universe" makes intuitive sense to me in this context, at least).
ddellacosta 2y ago
This is great stuff! As a Haskell fan who uses Elixir (and Erlang) in my day job, I'm really looking forward to seeing how we can leverage more of the new set-theoretic type features showing up in Elixir. Revisions seem like something I've never really seen before in any of the type systems I've used, so I'm excited to see how it can be leveraged in a real production system. Thanks for the post.

beders 2y ago

These are great examples of difficulties people will encounter in all popular statically typed languages sooner or later. I find the solution presented interesting but it is limited to the 3 operations mentioned. The alternative to this runtime schema checks and treating your data as data - the data you are working with is coming from an external system and needs to be runtime-validated anyways. Throw in some nil-punting and you can have a very flexible system that is guarded by runtime checks.

mrkeen 2y ago
Agreed that it is naive to assume that static types will keep some kind of consistency on the bytes that come in on the wire, but it misses the point. With static types, you do one transformation from bytes to a proper data type at the boundary. The static type information propogates bidirectionally deep into the guts of the system. If you're 10 layers in, and want to invoke getUserId() on an object, you just add it to your type. Now your endpoint can return 400s without you needing to add extra nil-checks somewhere (or multiple places) from layers 1 to 10 (which realistically will turn into 500s).
- Vampiero 2y ago
  Realistically you can design a runtime-checked interface that uses option types instead of nulls, thereby guaranteeing static correctness and preventing common pitfalls at the cost of making the usage pattern a bit more verbose.
- delusional 2y ago
  > but it misses the point. I don't think it misses the point as much as it's an entirely different point. When I talk to my coworkers about the uses of these automated marshaling systems at the boundary, they're not talking about correctness or "evolution". They talk about how annoying they find it to type. In the fingers hitting keyboard sense of that word. They explicitly don't want a change 10 layers deep to result in any error in the parsing layer. They want the magical system to just do something at runtime.
manx 2y ago

Groxx 2y ago

Yea, this is an issue rather near and dear to my heart (due to pain). I very much appreciate strong and safe types, but it tends to mean enormous pain when making small obvious fixes to past mistakes, and you really don't want to block those. It just makes everything harder in the long term. As an up-front caveat for below: I don't know Elixir in detail, so I'm approaching this as a general type/lang-design issue. And this is a bit stream-of-consciousness-y and I'm not really seeking any goal beyond maybe discussion. --- Structural sub-typing with inference (or similar, e.g. perhaps something fancier with dependent types) seems like kinda the only real option, as you need to be able to adapt to whatever bowl of Hyrum Slaw[1] has been created when you weren't looking. Allowing code that is still provably correct to continue to work without modification seems like a natural fit, and for changes I've made it would fairly often mean >90% of users would do absolutely nothing and simply get better safety and better behavior for free. It might even be an ideal end state. I kinda like the ergonomics of `revision 2` here, it's clear what it's doing and can provide tooling hints in a rather important and complicated situation... but tbh I'm just not sure how much this offers vs actual structural typing, e.g. just having an implicit revision per field. With explicit revisions you can bundle interrelated changes (which is quite good, and doing this with types alone ~always requires some annoying ceremony), but it seems like you'll also be forcing code to accept all of v2..N-1 to get the change in vN because they're not independent. The "you must accept all intermediate changes" part is in some ways natural, but you'll also be (potentially) forcing it on your users, and/or writing a lot of transitioning code to avoid constraining them. I'm guessing this is mostly due to Elixir's type system, and explicit versions are a pragmatic tradeoff? A linear rather than combinatoric growth of generated types? >It is unlikely - or shall we say, not advisable to - for a given application to depend on several revisions over a long period of time. They are meant to be transitory. An application, yes - applications should migrate when they are able, and because they are usage-leaf-nodes they can do that without backwards compatibility concerns. But any library that uses other libraries generally benefits from supporting as many versions as possible, to constrain the parent-library's users as little as possible. It's exactly the same situation as you see in normal SAT-like dependency management: applications should pin versions for stability, libraries should try to allow as broad of a range as possible to avoid conflicts. >Would downcasting actually be useful in practice? That is yet to be seen. I would pretty-strongly assume both "yes" and "it's complicated". For end-users directly touching those fields: yes absolutely, pick your level of risk and live with it! This kind of thing is great for isolated workarounds and "trust me, it's fine" scenarios, code has varying risk/goals and that's good. Those happen all the time, even if nobody really likes them afterward. But if those choices apply to all libraries using it in a project... well then it gets complicated. Unless you know how all of them use it, and they all agree, you can't safely make that decision. Ruby has refinements which can at least somewhat deal with this, by restricting when those decisions apply, and Lisps with continuations have another kind of tool, but most popular languages do not... and I have no idea how possible either would be in Elixir. --- All that probably summarizes as: if we could boil the ocean, would this be meaningfully different than structural typing with type inference, and no versioning? It sounds like this might be a reasonable middle-ground for Elixir, but what about in general, when trying to apply this strategy to other languages? And viewed through that lens, are there other structural typing tools worth looking at? [1] https://en.wiktionary.org/wiki/Hyrum%27s_law https://en.wiktionary.org/wiki/Hyrum%27s_law

Moosieus 2y ago

This is some interesting shit, I love it! At least that parts I think I understand :P > The goal of data versioning is to provide more mechanisms for library authors to evolve their schemas without imposing breaking changes often. Application developers will have limited use of this feature, as they would rather update their existing codebases and their types right away. Although this may find use cases around durable data and distributed systems. "Hard cutover" is definitely a lot less laborious, but often times incremental updates are necessary - large teams, existing tables and whatnot. To that end, I would foresee a lot of appeal in app dev when applied to database migrations.

harrisi 2y ago

Some initial concerns when thinking about this: - Understanding how it expands the surface area of both the API and discussion of a struct (and thus also libraries and dependencies of the librar{y,ies}). Now you don't need to ask someone if they're using v1.0 of some package, but also which revision of a struct they're using, which they may not even know. This compounds when a library releases a new breaking major version, presumably - `%SomeStruct{}` for v2 may be different from `%SomeStruct{}` v1r2. - Documentation seems like it would be more complex, as well. If `%SomeStruct{}` in v1.0 has some shape, and you publish `v1.1`, then realize you want to update the revision of `%SomeStruct{}` with a modified (or added) field, would there be docs for `v1.1` and `v1.1r2`? or would `v1.1` docs be retroactively modified to include `%SomeStruct{}v1.1r2`? - The first example is a common situation, where an author realizes after it's too late that the representation of some data isn't ideal, or maybe even isn't sufficient. Typically, this is a solved with a single change, or rarely in a couple or few changes. I'm not sure if the complexity is worth it. I understand the desire to not fragment users due to breaking changes, but I'm not sure if this is the appropriate solution. - How does this interact with (de-)serialization? I happen to be working with the SQLite file format currently, and I generally really enjoy data formats. It's not exactly the same as this, since runtime data structures are ephemeral technically, but in reality they are not. The typical strategy for any blob format is to hoard a reasonable amount of extra space for when you realize you made a mistake. This is usually fine, since previous readers and writers ought to ignore any extra data in reserved space. One of the things one quickly realizes when working with various blob formats is the header usually has (as a guess), 25% of it allocated to reserved space. However, looking at many data formats over the last several decades, it's extraordinarily rare to ever see an update to them that uses it. Maybe once or twice, but it's not common. One solution is to have more variable-length data, but this has its own problems. So, in general, I'm very interested in this problem (which is a real problem!), and I'm also skeptical of this solution. I am very willing to explore these ideas though, because they're an interesting approach that don't have prior art to look at, as far as I know. EDIT: Also, thanks for all the work to everyone on the type system! I'm a huge fan of it!

harrisi 2y ago
I forgot to mention, the typical situation for these things for added elements is to add `_ex` or the like, which is not a great solution. You can see this in various places in Erlang, especially around erl_interface and related aspects. On the flip side, what if you realize a data structure needs to remove elements? Say revision 2 adds a field, but revision 3 removes it?

airstrike 2y ago

That was an interesting read. Thanks for sharing and congrats on getting it out there. Two bits stood out and made me think, somewhat in disagreement: > If “data_schema” changes a user facing type, such as the Schema type above, in a backwards incompatible manner, its authors have to release a new major version. A new major version can be a fork on the road. Libraries that depend on “data_schema”‘s new version won’t accept the old ones. Old libraries that depend on “data_schema” have to be updated and potentially forced to also release a new major version, cascading the problem. If any package along the way is unmaintained, it can stall and complicate further downstream updates. I wouldn't call it a fork on the road. More like growing pains. This is to be expected of any dependency you have, and it's on you to keep your own code up-to-date. If the original Schema was indeed incorrect, it warrants fixing, even if it's an edge case. And then > In our v1 of Schema, we allowed name to only be a string(). In a statically typed language, we are effectively proving that all uses of Schema has a string() name. When we allow the name to also be nil in v2, that should not introduce bugs in our software yet because, by definition, there is no instance of Schema where the name is nil! > In other words, all existing code remains correct, but most type systems would immediately flag them as wrong, on the possibility they may receive a nil value. There must be a better way and that’s what we study in this article. Personally I don't think that what is proposed here is strictly better. I'd rather have to explicitly change my code to match the new shape of the Schema than to have it magically work. If I don't make changes now, I'm just punting that complexity for later and it's going to come back to bite me in some other issue that will be twice as hard to debug.