Data Invariants | Hacker News Reader

Data Invariants

buttondown.email

45 pointsTomte10 comments

First of all, that Interval type is insane. The Max of the interval [7, ∞) is 7!? What!? And (-∞, 7] and [7, ∞) are both OK but (-∞, ∞) isn't? As software engineers, it's our job to spot that whatever requirement is driving this type is absolute nonsense and we need to refuse to implement such a stupid data type and work back up the chain until whatever stupidity led to this situation is resolved. I would literally refuse to write this code, and so should you. This is the difference between a "programmer" and a "software engineer". A programmer says "yup, sure, interval, got it", and a software engineer says "hell no, that's insane, something is very wrong."

Secondly, you're mutating an interval!? Holy moly mother of god that gives me nightmares. There are a few data structures where mutation makes sense, where they're used privately as part of an algorithm and then thrown away or frozen. Other than that, there is absolutely no excuse whatsoever to make data types mutable. There are no reasonable arguments to made for making an interval like this mutable; any argument you give me could be extended to making an int mutable, which is absolute crazy nonsense.

Seriously, this code is absolutely terrifying. "Data Invariants" as described here sounds like someone talking about techniques for setting up guardrails along the road because they constantly drive off of it. It sounds like maybe you need to go back to driving school instead of worrying about how to build better guardrails.

I have a feeling that somehow whatever drove this blog post originally wasn't adequately described here because as you mention, the semantics of "max" make no sense here.

> The Max of the interval [7, ∞) is 7!? What!? And (-∞, 7] and [7, ∞) are both OK but (-∞, ∞) isn't?

Yup, you got it, both of those are exactly correct. I needed it for Beamer `\onslide`-like functionality in another context.

> I would literally refuse to write this code, and so should you. A programmer says "yup, sure, interval, got it", and a software engineer says "hell no, that's insane, something is very wrong."

This was for a personal tool that cut down on a lot of repetitive work for me.

> Seriously, this code is absolutely terrifying.

This was for a weekly email newsletter, I wasn't going to spend hours finding the perfect example of data invariants when a simple one was enough to showcase the idea.

When I read blog posts about software engineering subjects, I automatically go into "let's learn about the discipline of software engineering" mode, and there's where that very critical eye comes from. I don't want to discourage people from writing informative blog posts, but I also think there is a lot of really mediocre information out there for a discipline that is struggling to find its "professionalism". So your sentiment of "I wasn't going to spend hours thinking hard about the best possible example to illustrate my point" really has me at odds with myself. I'd much prefer that people who write purportedly informative posts about deep subjects in the discipline do spend hours and hours thinking about it. On the other hand, I've spend thousands of hours thinking on these subjects and I've never written a blog post myself because I always fall into a spiral of feeling like it's not good enough to publish.

Software developers are reading your post, and if they enter into a mode of "here's a new concept to learn from an obvious expert", they may subconsciously (or consciously) absorb bad habits from your examples. Your blog post may actually do more harm than good to the discipline. It might be different if you had outright stated "hey these examples are from hobby project and not good examples of actual good code and you should not copy what I'm doing because it's not suitable for a professional environment." But that would rather weaken the entire effect of the blog post, wouldn't it? If your examples are not appropriate for a professional context, shouldn't you have a disclaimer that says "this blog post is only for hobbyists and is potentially misinformative for professional software developers"? Otherwise simply saying "well this is just a hobby project so it doesn't need to be good code" is a cop-out. You published this, and professional software developers are reading it.

There's not an easy answer. I want people to blog about software engineering concepts, and I don't want the bar to be set so high that nobody ever feels like their post is good enough to publish. Yet spending a couple hours finding the best possible example to illustrate their point (instead of code that is literally inappropriate in a professional context) does not seem like too high a bar to me. The best I can do is rip apart things I see as serious problems in educational posts, in the hopes that developers can read both points and take the best from each.

> The easy way out is to say that invariants are “observable” properties and nothing can observe the broken invariant in the middle of the method call.

Unless you are invoking user-defined functions in the middle that can observe it. This can be tricky for example in C++. The user-defined functions can be explicit callback arguments, but as simple as copy/move-constructors or conversion operators can trip you up.

For C++ standard library containers the public member functions are not guaranteed to be reentrant for example (the wording for this is not great though).

https://godbolt.org/z/xKMoxrr3E

This might be a contrived example. But I actually had something like this happen when I wrote a generic memoization class that used an unordered map under the hood, and then I tried to memoize a recursive function. It ended up calling the same map's `try_emplace` function recursively, which blew up spectacularly with abseil's implementation of unordered_map.

> The easy way out is to say that invariants are “observable” properties and nothing can observe the broken invariant in the middle of the method call.

Which is why object's private/internal methods in general should not calling its public methods: public methods are usually written in the way that expects the object to be in a consistent state at the start of the call, and in the middle of a private/internal method it very much likely is inconsistent.

That's something I've personally been burned with and learned the hard way. Know thy methods' preconditions!

I was thinking, a function that checks for preconditions (assertions) will be necessarily slower than one that skips those checks. The code will be smaller, but not necessarily easier to read if data quality assertions are omitted. Graceful failure also can be handled on a case by case basis - something assertions don't solve.

There's also a large but not unbounded search space when it comes to numerical values. Some things (like division by zero) are easy to check, but other things like valid strings or checking that a graph data structure is shaped a certain way - the search space is potentially enormous. That's why some invariants (ex: assert i <= 0) are easier to define than others (ex: i is prime)

That's not to say data invariants aren't useful - our function would not work if the assumptions it depends upon aren't true.

Point is, proving an invariant involves executing code, either at compile or at runtime - and there's no guaranteeing that code coming from user input or databases or remote API calls satisfy the invariant.

> there's no guaranteeing that code coming from user input or databases or remote API calls satisfy the invariant

The idea is that you should check the invariant at the "boundaries" of your code. Then you can write your internal routines assuming that the invariant holds.

This is a developing pattern in Idris libraries that use "proof carrying" types. You write a function that returns 'Either DataValidationError (DPair Foo fooIsValid)' and use that to construct your internal data types as well as a proof that the data satisfies whatever invariants you need. It's just an application of the "parse, don't validate" principle, extended to use dependent and proof-carrying types.

The trickier scenario is when the data is already "internal" but is located outside of the application, like in a database. In that situation you either have to take the performance hit of doing internal integrity checks, or you assert that the invariant holds without checking it, and write tests accordingly + possibly out-of-band checking for data integrity.

For dynamically-typed languages and/or when using runtime "contracts", I think Clojure handles this by disabling some or all precondition checks at runtime, but expects them to be turned on during testing.

Those invariants look to me pretty much like additional constructor arguments in languages with dependent types. Which both do "Make Illegal States Unrepresentable" and can provide "natural" ways to represent the data, along with the additional arguments (those proving the desired properties).

To be more precise, in Idris something like:

  data Interval : Type where
    From : (start : Int) -> Interval
    Until : (end : Int) -> Interval
    Bounded : (start : Int) -> (end : Int) -> {auto lt : LT start end} -> Interval

could work (I haven't used Idris in a bit, so this might not compile as is).

With this declaration this would compile:

  intervals : List Interval
  intervals = [ From 2
              , Until 5
              , Bounded 2 5
              ]

while this would not:

  interval : List Interval
  interval = Bounded 5 2

However, supplying that "lt" proof (implicitly or explicitly) could become tedious in some cases. The proof burden is often kind of a problem with dependent types. In such a case, the "start + offset" based approach might be preferable, even if it leads to a more complicated API.

Reply on news.ycombinator.com