Make invalid states unrepresentable (2023)
geeklaunch.io
geeklaunch.io
After a while it occurred to me that all state was duplicate/triplicate/..., e.g. a checkbox on screen and a boolean field. Most bugs amounted to inconsistencies between the duplicates. So we wrote for each form 2 big methods: One copied the records to the UI, the other the UI to the record. All listeners became a 3 step process: Copy complete UI to record, do the change only in the record, copy complete record to UI.
In a way this was wasteful: Typing 3 characters would enable or disable most GUI elements 3 times. But computers had become fast enough that this was unnoticeable. The dynamic of the program changed: instead of tiny mistakes in the code spiraling out of control, they would disappear as the next user action would most probably fix them. Bugs basically dried up overnight after what amounted to a small code change.
In this case, it was too late to make invalid states unrepresentable, but we managed to declare 1 part of the state correct, and derive all the other state from it. I learned a lot about state management from that experience.
It wasn't, that's exactly what you did, albeit not with types, but by removing redundancies from the state. It's the same reason why normalizing relational databases is a good idea.
the thing with using types to make unrepresentable state is that it ensures the compiler is the one checking.
By doing it "manually" this way, you're not saving much effort. You still had to make the analysis of which state is valid, and to code it up (hopefully without a mistake). The state of the program can also temporarily be invalid - just happens to fast for the user to notice (thus "fixing" the bug).
It's probably the best that could've been done other than a rewrite, but make no mistake - it's not the ideal.
Isn't this the essential philosophy of React?
The other approach is INotifyPropertyChanged-style: an event for every change, which is supposed to propagate to all listeners, but only propagate if the value is different. It sounds like this is the one that had failed in the project you were given.
> Typing 3 characters would enable or disable most GUI elements 3 times
I don't think this matters so long as you can coalesce all the redraws. See also "immediate mode" GUIs: if you always redraw everything from the canonical state, which modern computers are extremely fast at, a lot of complexity goes away.
In a way, the core change in mindset was realizing that computers got fast enough for this architecture to be reasonable. Some of the devs had worked with a machine having 1MB of memory shared by everyone, and snapping out of that is hard. I remember someone on that project lamenting we would be wasting whole kilobytes of memory. Funny even then, but today I recoil from electron, much for the same reason.
Today, you'd be absolutely right.
This is the essence of model, view, controller, and also one of the very first use cases for it!
Always separate the truth state from everything derived.
Especially the UI. Ideally have a single "render" method that updates your complete UI from the application state.
A third piece / concept I often circle back to is a lot more subtle and difficult to grok: “Names are not type safety” (https://lexi-lambda.github.io/blog/2020/11/01/names-are-not-...)
month: 1..12;
letter: 'A'..'Z';
To be clear:
- Many things have improved and I'm glad I don't have to write my software in Pascal[1] today.
- I don't really miss the generalization of this feature. Things like refinement types would be nice, but what Pascal provides would be enough to make life so much better.
It also works for arrays, by the way, which very elegantly sidesteps the 0-based/1-based controversy.
FooPerMonth: array[1..12] of Foo;
LandingsPerRouletteWheelPos: array[0..36] of Landings;
type Digit is range 0 .. 9;
type Unsigned_Byte is mod 2 ** 8;
type Binary_Floating_Point is digits 15 range -1.0 .. 1.0;
type Binary_Fixed_Point is delta 2.0 ** (-32) * Pi range (-Pi / 2.0) .. (Pi / 2.0);
type Decimal_Fixed_Point is delta 0.01 digits 5; type
TMonth = (mJan = 1, etc);
TFooPerMonth = array[TMonth] of integer;You can have those semantics in .net, because any hashable can be a dictionary key. It will have a small performance penalty, which won't matter in 99% of cases. You could roll your own collection and get O(1).
F# lets enum values be records, which is the most elegant solution IMO for manageable counts and fields.
(It's been long enough I'm not completely sure of the syntax) Time : Array [2000..2100, 1..12, 1..31] of OneDayInfo;
Avoid allocating the 2000 years in the past while allowing directly indexing with the year field.
And you could use enum types as array indexes. In C# you're always casting them to int whenever an enum is an array index and every cast is a case where the compiler won't have your back in hunting for errors.
And it did *not* use duck typing.
Month: 1..12 DaysOfChristmas: 1..12
You couldn't assign which day of Christmas to a month.
The stricter the compiler the fewer bugs will even compile and the faster you'll find the problem.
As for his color assignment issue--you still need to be able to set it to "purple", but representing it his way pushes this back to whatever routine parsed the configuration. There's only one place that needs to make the check and anything bogus will be caught during startup.
> Types delineate the set of legally representable states |ℝ| in your application
and
> |ℝ|≥|ℙ|
Which sets off my "math" alarm. The less out-and-out math used to make a point about programming, the better, I think. This article is actually fairly good and doesn't get very mathy beyond the intro, but it still jumps out at me and made me wary to continue.
So this isn't about purity, it's about being declarative. i.e. make your code say what it accepts, instead of writing board/implicit acceptable inputs that inevitably forget cases and crashes.
If you limit what you accept as inputs then you can stop worrying about downstream error handling and debugging.
Imagine if an electrical engineer said this. Or an aerospace engineer. Or any real engineer.
With that out of the way, isn't it better if software development concepts can be explained with less math-heavy notation while keeping the math notation for the cases precision is needed?
I for sure remember a dwindling amount of the math from my statistics bachelor in my head after 15+ years. I'm able to recollect it after re-reading some material, things usually click back in place but I won't be doing that unless it's very necessary.
I've yet to see a software project where an software engineer was given much leeway in how a project was run, scoped, or where any of their concerns about the scope, schedule, or lack of an actual plan were taken seriously... I'll gladly trade being falsely labelled an engineer for overtime pay to cleanup the mess on schedule yet again.
So?
Lambda calculus and number theory are significantly hairier.
The actual example in the article isn’t that great but my point is generally it’s a valid way to explain or demonstrate something. That’s part of the reason we learn it.
No, only an audience of mathematicians grasp concepts explained exclusively with maths.
Why do you find this surprising? It's no more surprising than "Only an audience of carpenters grasp concepts explained exclusively with joinery terms".
Would you, with a a straight face, make the claim that explaining something using terms like "Cheek", "Mortise & Tenon", "long grain", "Dado" and "Birdsmouth" is a valid way to explain something unrelated to carpentry?
Why then claim that using mathematics terms to explain something unrelated to that specific maths is a good idea?
I mean, this article is a good example: not only does the article get the maths wrong, the maths involved is unrelated to what it the article is trying to explain.
In most cases, especially cases of software engineering, as opposed to computer science, the math gets in the way of the point. It was never needed, it just served to obscure the topic. Plus, I'm not an engineer, and I'm not doing mathematics in my daily life. I don't think like a mathematician, I don't work with cardinalities, or set theory, or integrals. At most I deal with some multiplication and powers-of-two. Maybe a ratio here and there. If I was a graphics programmer, which I thankfully am not, I'd toss in some matrix algebra maybe. But my career doesn't involve anything requiring the use of ℝ. What it does involve, is thinking about composability of systems, debugability, simplification of processes, and otherwise making sure things work and can be understood by future maintainers. The article's topic is useful, but making things mathy for the sake of it is a navel gazing distraction.
it's not marred, but formalized by mathematics.
Maths is very unambiguous. It makes it so that you cannot interpret it wrong, as long as you learn the meaning of the symbols. The transformation of these symbols are logical operations, and follows on from previous operations.
By describing processes or thoughts this way, it ensures that what you say is formal - aka, someone else can follow the logic _exactly_ from the assumptions/axioms.
It also allows you to overlay proven theorems from other fields of maths and apply it to your current situation. By doing so, you can transform your problem to a known solved problem, and therefore, have a solution. This solution might be complicated and require knowledge from that field unrelated to your problem, but i dont think that's a problem with maths itself - it's a sign of your own deficiency.
Finally, maths forces you to think systematically. It forces your brain to adopt a style of thinking that most people find difficult, but it is what it takes to solve problems wholistically.
But I think it is often counterproductive when evangelizing a concept or explaining something to software developers.
And 2), most engineers are not super comfortable with even relatively basic mathematical notation like this. If your audience is software engineers (and specifically not mathematicians), it’s better to say what you mean, in plain terms. While 80% of folks might know what you mean, it’s not worth losing the other 20%.
On the other hand, if the math is the point, then it is more than appropriate.
I might be a bit out of date here. I can imagine how it could be true for bootcamp developers who never had relevant formal education, but I don't think they are a majority. Most engineers go through some kind of higher education program, be it CS or CE, and it normally includes a significant amount of math. How can you get around getting comfortable with it?
If most engineers truly are not familiar with basic math notation, the solution should be to teach more math to engineers, not purposefully explain things in a less formalized way.
~~I KNOW I used the terms developer/engineer interchangeably, don’t kill me~~
Curry and Howard have some bad news for you https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
record Point(double X, double Y);
record Point {
public required double X { get; set; }
public required double Y { get; set; }
}
But yes, it's good that languages are moving in this direction.
That said, there is a vast design space between Javascript/Python and dependent types. Plain old ADT suffice in 95% of cases, yet the only mainstream language with ADTs is Rust. This is a shame.
Swift, Kotlin, Scala and Typescript all support forms of ADTs, just with different names.
- Swift calls them "enums" (like Rust)
- Kotlin and Scala has "sealed classes"
- Typescript has "discriminated unions"
Kotlin (and even Java 15+ nowadays) can emulate ADTs with sealed classes, but the ergonomics are incredibly bad and the ecosystem is not build around the concept.
Scala has ADTs, but I would put Scala in the same category as Haskell or OCaml. A niche language.
Typescript does not have ADT, they have union types. You can build a discriminated type out of a union type, but you have to do this manually. This misses on the ergonomics of using ADTs plus people do it in different ways.
ADTs in one way or another are becoming more mainstream, but they are very far from being accepted by default.
I quite like Typescript's approach. You do get exhaustive switch-case matching, so that's like 80% of what I want out of sum types. Typescript also lets you enforce that a type is one of the variants of a sum type, something which e.g. Haskell doesn't let you do. I assume this is a function of Typescript doing union types, but it's pretty convenient.
Definitely see ADTs becoming mainstream, because they are genuinely useful. Biggest gap to adoption imo is that no SQL database supports sum types or anything equivalent.
I can see that if I made the branch return a string, Typescript will correctly show the "Not all code paths return a value" error
My team lead used to shoot down ideas if they were "too complex". Correct and wise, right?
Except that this numskull created reams of functions that took untyped python dictionaries, did something, and passed them to other functions.
Early on, he bolted a giant mess of validation onto the perimeter. This did add value... but most data invalidity arose inside the fucking app!
He had a great eye for the complexity of abstractions, but was completely blind to the complexity of doing simple things in convoluted ways.
It was miserable. Any random PR could pass all the integration tests we had and still blow up prod, because there were orders of magnitude more code paths than lines of code.
I progam in Lean, a language that makes it extremely easy to state requirements and constraints. Using dependent types, you can even reach down into the implementations of function arguments, demand specific ranges for numerics etc. But this imposes a correspondingly large burden on the function caller! If you have a function
/-! pass : short for pain in the ass -/
def pass (n : Nat) (h : 0 < n && n < 5) := n^2
One way to deal with this without utter insanity is to create a certification monad and make these functions monadic, adding certificates to the return type:
def myfun (args: _) (reqs: _) : (returns : _) (certificates : _) := sorry
Humans are not ready for perfect information representation.
With CUE, we are trying to solve this exact problem.
[0] -- https://zerotomastery.io/blog/rust-typestate-patterns/
what's the difference here between state and data? Isn't data more generic, and we can have the title 'make invalid data unrepresentable'?
Because I have this instinct to do what I call in my mind and to my friend 'ddd', for 'data driven programming'. It translate by first thinking on my global inputs, outputs, and transformations, then writing the data structure (I learned with C), then prototyping the core functions (basically I write the .h before the .c).
Is it the same thing? Let the data write the code (or state, and they're the same thing here?) or did I miss something important?
A computer program can be split into 3 large parts: input, process, output. And invalid data, in my opinion, only concerns the first part, whereas invalid states can be found throughout all parts of the program due to e.g. bugs.
That makes "make invalid states unrepresentable" more generic than "make invalid data unrepresentable". Or to put it in another way: invalid data can lead to invalid states, but not all invalid states are due to invalid data.
IMO "state" is a better fit for the concept that this is getting at. The point is to stop the program getting into an invalid state, not to stop the program operating on invalid data, because a program might need to process data that's invalid in some sense, and because the program state is something a bit more active than "data" (e.g. having the right data at the wrong stage of execution is also an invalid state, even though it isn't exactly "invalid data").
A checkbox represents a single value. A collection of checkboxes represents something different, the state.
So for example, if I ever see a CHAR(1) column that looks like it's meant to hold a boolean of some sort, the best thing is to immediately lock it down to a strict subset (preferably not NULL) of 2 states like ['Y'|'N'].
I still have nightmares about a db schema that grew a fungus of boolean representations, and massive amounts of code checking for y,n,Y,N,0,1,T,F,t,f all of which were used by different teams at different times. Constraints would have stopped all that.
Here's the docs for Postgres: https://www.postgresql.org/docs/current/ddl-constraints.html
I feel such an extension will immediately find its audience.
struct AdminNote {
id: String,
text: String,
category: CategorySpecificData,
}
enum CategorySpecificData {
GeneralRequest,
InitialRequestForm {
appliesToBasicRequestDetails: bool,
appliesToSubjectAreas: bool,
appliesToAttendees: bool,
},
SupportingDocuments,
ConsultSession,
AdviceLetter {
appliesToMeetingSummary: bool,
appliesToNextSteps: bool,
},
}
As far as making this a Postgres extension - I'm not sure how useful it would be when the application language doesn't have a notion of sum types. Thinking about it, what might be more useful would be a language-specific library for data validation/constraints that sets up the database constraints as well. I'm not sure, though.
[1] We weren't using Rust, this was in Go, but I figured this was the most succinct way to summarize it. Our GraphQL schema for this type was basically the equivalent of this.
[2] https://github.com/CMSgov/easi-app/blob/main/migrations/V164...
Though I really have to wonder if there couldn't be a way to generate the SQL constraints out of the data declaration as well. Golang's struct tags are likely not going far enough though.
So I’ve learned that the constructive approach is awkward to work with in practice, and the newtype-wrapper approach is not type safe. What would be an example to implement the `OneToFive` example properly and in a type-safe way, then?
https://www.youtube.com/watch?v=IcgmSRJHu_8
the talk is Elm lang focused, but the concepts still apply to other languages.