3 ms·

The problem I think is that when you define an invariant, you are also defining an infinite number of "implicit" invariants. And it's hard to know a priori whic

by yen223 3y ago

The problem I think is that when you define an invariant, you are also defining an infinite number of "implicit" invariants. And it's hard to know a priori which of those implicit invariants is not an actual invariant over time. Take a simple User type type User { name: string email: string } This describes some obvious invariants - that a User will have a name and an email. But it's also describing some less obvious invariants, e.g. that a User will not have a phone number. This has implications if a phone number ever does get added to a User type, and your system has to deal with two different versions of Users. (This isn't just an academic problem - the problem of trying to evolve fields over time is the reason why Protobufs got rid of the idea of a "required" field.) And this is an example of a very simple implicit invariant. In practice, systems that interact with each other will give rise to emergent behaviour that one might think is always true, but is not guaranteed.

_ZeD_ 3y ago
>>> (This isn't just an academic problem - the problem of trying to evolve fields over time is the reason why Protobufs got rid of the idea of a "required" field.) if this is the reason of the drop of the required field it doesn't seems smart to me. They are conflating the definition of a scheme with the scheme evolution logic. And there are multiple ways to deal with the latter (like adding a schema version, for instance)
- yen223 3y ago
  I don't have a very strong opinion about that change specifically. I think they could have kept their cake and ate it too by solving the schema evolvability some other way, but I also suspect those other ways will come with tradeoffs that are also not pleasant. But, the point is schema evolvability is a real problem, and it's often not one that a lot of engineers give a lot of thought to, even those who live in very strict statically-typed worlds.
- larsrc 3y ago
  Some "required" fields in very commonly used protos ended up being unused, but everybody has to fill them out all the time. If they didn't, the proto wouldn't even parse, by design. Protobufs explicitly do not have a built-in version system (though of course you could add an optional field for it), presumably because it is better to inspect the data than build in assumptions that a certain version overs a certain invariant.
atoav 3y ago
This is why I tend to like to use strong type systems where possible and necessary. struct LoginUser { name: UserName, email: Email, phone_number: Option<PhoneNumber>, } First the user type should reflect the function of the user. This is one that is allowed to log in (of course overly simplified). You can then also have a OnboardingUser, a ArchivedUser and so on. And if you want to transition one between those different types you need to ensure the fields are there. This is easy to test and clear. The other thing is to use types for fields that have hard verification requirements. You can still have them behave mostly like strings for reading, but you can ensure that an Email in a LoginUser never contains an unverified Email, by first verifying the email string in the OnboardingUser and only converting it into the Email type once it is guaranteed to be a valid email. Because you use a special type tacking on further things like storing a date when this verification happened last is easy, just put it into the type as well. Lastly the phone number is an Optional type that wraps a PhoneNumber type. This way it can either be None or Some<PhoneNumber> (this uses the Rust typesystem, but the principle would work elsewhere), the phone number should be verified the same way, ideally relying on a well tested method that also fixes the formatting at the same time. Now in Rust if some part of the system didn't handle a user that has a phoneNumber your code won't compile, because from the standpoint of the old code this would now be an entirely new, unknown type never seen before. Sure you could step through your code and explicitly not handle it on purpose because you want back to a running system fast, fail to add a TODO and then later forget about having to do it, but that would be entirely on you. Now those hard typesystem constraints become even more valuable when dealing with external systems. Your type should represent all assumptions you are making about the data and test those on each import. Of course you then will have import failures if the import source changed, but we want that to fail if it changes. What we don't want is the thing silently chugging the input into the wrong pipe or invalid phone numbers to be stored because the source system decided to split them up into the prefix and the rest.
- yen223 3y ago
  Static types are really good for describing invariants, I definitely agree. But it does also describe a lot of implicit invariants. The LoginUser you've defined has the implicit invariant that a LoginUser only has 3 fields. It is very possible for someone to write a function that relies on a LoginUser only ever having 3 fields, which then breaks if you ever extended LoginUser. This is similar to the example that the article mentions at the start, where a thing that someone assumed would always fit in one memory region no longer did, and that caused all kinds of problems. Those kinds of implicit invariants are the ones that are tricky to make explicit, even in strongly-typed languages.
cryptonector 3y ago
> But it's also describing some less obvious invariants, e.g. that a User will not have a phone number. That's not right. For one, the `User` type might be extensible (what language is this?). For another one can always add additional metadata about users elsewhere -- think of how you might do it in a relational database. > (This isn't just an academic problem - the problem of trying to evolve fields over time is the reason why Protobufs got rid of the idea of a "required" field.) Protobufs is the poster boy of bad reinvention. ASN.1 got all these things right over a lot of time, and instead of taking the best of it and leaving out the worst of it, everyone is constantly reinventing ASN.1 badly. And yes, ASN.1's evolution was "academic" in many ways, and its authors blazed trails. ASN.1 never had a "required" anything, but it did (and does) have an OPTIONAL keyword. The reason I mention extensibility above is that ASN.1 has been through the whole academic study of extensibility over several decades: - since the original encoding rules were tag-length-value, in the beginning you could just add fields as long as you knew the recipient could handle them (e.g., by ignoring unknown fields) - when that proved unsatisfying they added extensibility markers for denoting "here go extensions" vs "no extensions allowed", and "these are version 2 extension fields", and so on, and not just fields but also things like INTEGER ranges, enums, etc. - they also put a lot of effort into formalizing the use of "typed holes" (things like {extension-type-ID, <encoded-value-of-that-type>}), and they did this pretty much before any other schemes. (The wikipedia page on comparing serialization schemes[0] refers to "typed holes" as "references", FYI.) Extensibility is fairly well covered in many serialization formats now, like XML for example, but still fairly poorly covered in others. In SQL and relational systems in general one can always add additional fields via tables to JOIN on, and often by adding columns to existing tables. Extensibility is a big deal, and serious systems will have had serious thought put into it. [0] https://en.wikipedia.org/wiki/Comparison_of_data-serialization_formats

by yen223 3y ago

_ZeD_ 3y ago

>>> (This isn't just an academic problem - the problem of trying to evolve fields over time is the reason why Protobufs got rid of the idea of a "required" field.) if this is the reason of the drop of the required field it doesn't seems smart to me. They are conflating the definition of a scheme with the scheme evolution logic. And there are multiple ways to deal with the latter (like adding a schema version, for instance)

yen223 3y ago
I don't have a very strong opinion about that change specifically. I think they could have kept their cake and ate it too by solving the schema evolvability some other way, but I also suspect those other ways will come with tradeoffs that are also not pleasant. But, the point is schema evolvability is a real problem, and it's often not one that a lot of engineers give a lot of thought to, even those who live in very strict statically-typed worlds.
larsrc 3y ago
Some "required" fields in very commonly used protos ended up being unused, but everybody has to fill them out all the time. If they didn't, the proto wouldn't even parse, by design. Protobufs explicitly do not have a built-in version system (though of course you could add an optional field for it), presumably because it is better to inspect the data than build in assumptions that a certain version overs a certain invariant.

atoav 3y ago

This is why I tend to like to use strong type systems where possible and necessary. struct LoginUser { name: UserName, email: Email, phone_number: Option<PhoneNumber>, } First the user type should reflect the function of the user. This is one that is allowed to log in (of course overly simplified). You can then also have a OnboardingUser, a ArchivedUser and so on. And if you want to transition one between those different types you need to ensure the fields are there. This is easy to test and clear. The other thing is to use types for fields that have hard verification requirements. You can still have them behave mostly like strings for reading, but you can ensure that an Email in a LoginUser never contains an unverified Email, by first verifying the email string in the OnboardingUser and only converting it into the Email type once it is guaranteed to be a valid email. Because you use a special type tacking on further things like storing a date when this verification happened last is easy, just put it into the type as well. Lastly the phone number is an Optional type that wraps a PhoneNumber type. This way it can either be None or Some<PhoneNumber> (this uses the Rust typesystem, but the principle would work elsewhere), the phone number should be verified the same way, ideally relying on a well tested method that also fixes the formatting at the same time. Now in Rust if some part of the system didn't handle a user that has a phoneNumber your code won't compile, because from the standpoint of the old code this would now be an entirely new, unknown type never seen before. Sure you could step through your code and explicitly not handle it on purpose because you want back to a running system fast, fail to add a TODO and then later forget about having to do it, but that would be entirely on you. Now those hard typesystem constraints become even more valuable when dealing with external systems. Your type should represent all assumptions you are making about the data and test those on each import. Of course you then will have import failures if the import source changed, but we want that to fail if it changes. What we don't want is the thing silently chugging the input into the wrong pipe or invalid phone numbers to be stored because the source system decided to split them up into the prefix and the rest.

yen223 3y ago
Static types are really good for describing invariants, I definitely agree. But it does also describe a lot of implicit invariants. The LoginUser you've defined has the implicit invariant that a LoginUser only has 3 fields. It is very possible for someone to write a function that relies on a LoginUser only ever having 3 fields, which then breaks if you ever extended LoginUser. This is similar to the example that the article mentions at the start, where a thing that someone assumed would always fit in one memory region no longer did, and that caused all kinds of problems. Those kinds of implicit invariants are the ones that are tricky to make explicit, even in strongly-typed languages.

cryptonector 3y ago

> But it's also describing some less obvious invariants, e.g. that a User will not have a phone number. That's not right. For one, the `User` type might be extensible (what language is this?). For another one can always add additional metadata about users elsewhere -- think of how you might do it in a relational database. > (This isn't just an academic problem - the problem of trying to evolve fields over time is the reason why Protobufs got rid of the idea of a "required" field.) Protobufs is the poster boy of bad reinvention. ASN.1 got all these things right over a lot of time, and instead of taking the best of it and leaving out the worst of it, everyone is constantly reinventing ASN.1 badly. And yes, ASN.1's evolution was "academic" in many ways, and its authors blazed trails. ASN.1 never had a "required" anything, but it did (and does) have an OPTIONAL keyword. The reason I mention extensibility above is that ASN.1 has been through the whole academic study of extensibility over several decades: - since the original encoding rules were tag-length-value, in the beginning you could just add fields as long as you knew the recipient could handle them (e.g., by ignoring unknown fields) - when that proved unsatisfying they added extensibility markers for denoting "here go extensions" vs "no extensions allowed", and "these are version 2 extension fields", and so on, and not just fields but also things like INTEGER ranges, enums, etc. - they also put a lot of effort into formalizing the use of "typed holes" (things like {extension-type-ID, <encoded-value-of-that-type>}), and they did this pretty much before any other schemes. (The wikipedia page on comparing serialization schemes[0] refers to "typed holes" as "references", FYI.) Extensibility is fairly well covered in many serialization formats now, like XML for example, but still fairly poorly covered in others. In SQL and relational systems in general one can always add additional fields via tables to JOIN on, and often by adding columns to existing tables. Extensibility is a big deal, and serious systems will have had serious thought put into it. [0] https://en.wikipedia.org/wiki/Comparison_of_data-serialization_formats