[HN Gopher] Data Invariants
___________________________________________________________________
Data Invariants
Author : Tomte
Score : 40 points
Date : 2022-09-07 13:07 UTC (1 days ago)
(HTM) web link (buttondown.email)
(TXT) w3m dump (buttondown.email)
| swagasaurus-rex wrote:
| 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.
| nerdponx wrote:
| > 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.
| feoren wrote:
| 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.
| Tainnor wrote:
| 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.
| hwayne wrote:
| > 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.
| defanor wrote:
| 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).
| Tainnor wrote:
| 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.
| Joker_vD wrote:
| > 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!
| planede wrote:
| > 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.
___________________________________________________________________
(page generated 2022-09-08 23:03 UTC)