9 ms·

Make invalid states unrepresentable (2023)

103 points by satvikpendem 3y ago

FrankWilhoit 3y ago
Strong typing is like violence: if it isn't solving all your problems, you must just not be using enough of it.
- hi-v-rocknroll 3y ago
  Forth is tic-tac-toe and dependent typing is global thermonuclear war.
  - actionfromafar 3y ago
    It would then seem, the only winning move, is not to play.
    - hi-v-rocknroll 3y ago
      How about a nice game of Go?
      - 0atman 3y ago
        10/10, no notes XD
- Leo_Germond 3y ago
  I love that, going to reuse that one
  - FrankWilhoit 3y ago
    Don't credit me, it's not original, but I don't know the actual source.
    - another2another 3y ago
      First time I heard it, it was about XML. So, quite a while ago.
johann8384 3y ago
I thought this was going to be some political thing about states and congress.
klysm 3y ago
This principle has served me well for a long time, but it’s definitely a trade off space. We want to enforce as many invariants as possible through the type system, but more invariants requires more complexity. Eventually you run into dependent types etc.
- Leo_Germond 3y ago
  I would say it's a tool with an optimal point that is located along the "heavy use" side. I think it is interesting to think of them as solidifying your specification. As such if your spec is still changing or it is unclear (e.g. first impl draft, example code...), you should use some lightweight types, whereas a public API should have types that encode basically everything your comments can say about the values, operations, and memory representation of the parameters. That would be the point where I would consider that defining my types is "done" and I would consider switching to e.g. moving the functiona around instead (there are lots of hanging fruits in safe by construction approaches, that might not even require types - can't shoot yourself in the foot if I remove the footgun entirely)
- thom 3y ago
  There’s no shame in just having complex constructors to check some invariants in non-structural ways. At least you still capture and enforce the transition.
  - 4ad 3y ago
    That only works if your language is value-oriented, but most existing languages use references and mutation extensively.
    - int_19h 3y ago
      I think that's too broad and somewhat outdated. C++ has const, for example, and you're expected to use it. Java and C# give you final/readonly, and not only that, but immutability is becoming more idiomatic, with the language increasingly encouraging it. For example, in modern C#, record Point(double X, double Y); is immutable, whereas the mutable equivalent is the much more verbose: record Point { public required double X { get; set; } public required double Y { get; set; } } Java goes even further by not even having syntax for mutable records - if you want something like that, you have to write it out as a regular class.
hi-v-rocknroll 3y ago
One of the grossest large codebase anti-pattern is god state objects. One of the worst I've seen had to do with the state of conference call. Depending on the state, zillions of properties were or weren't valid. It was a huge, fucking mess that often allowed invalid states to creep in via edge-cases that led to unrecoverable states.
Animats 3y ago
Classically, this is a problem in hardware logic design. It's desirable that logic circuits not be able to lock up in an invalid state. So having a state machine where invalid states cannot be represented is useful. Hardware without this property tends to need reset buttons.
- YorkshireSeason 3y ago
  The abstract concept here is liveness, aka "eventually something good will happen". In practise, liveness alone is insufficient because a locked up program/processor is indistinguishable from a very slow program/processor. So you really want bounded liveness, along the lines of "within X time units, something good will happen".
orwin 3y ago
I have a question for the author or anyone smart enough to understand the whole post: 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?
- orangeboats 3y ago
  The way I understand it, "state" refers to any point in time during the execution of a program. 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.
- lmm 3y ago
  Do you think "state machines" should be called "data machines"? Why or why not? 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").
  - orwin 3y ago
    Very insightful (you and your siblings), thank you all. I think I have a fundamental misunderstanding of what a state is, maybe because I mostly practice responding to external state changes? I don't know, I'll think on that. Thank you again.
masklinn 3y ago
A companion piece to this idea (previously at Oleb’s “making illegal states unrepresentable: https://oleb.net/blog/2018/03/making-illegal-states-unrepresentable/ https://oleb.net/blog/2018/03/making-illegal-states-unrepres...) is “parse, don’t validate”: https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/ https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va... 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-type-safety/ https://lexi-lambda.github.io/blog/2020/11/01/names-are-not-...)
vsnf 3y ago
I'm sympathetic to this concept, and it's one I employ from time to time in the various codebases I own, but the type of person to advocate for this kind of thing is also the kind of person to write stuff like > 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.
- hnbad 3y ago
  I second this as I find that usually the solution that is the most mathematically pure is usually also the one completely inadequate at handling the complexities of real-world applications and end up having various extremely impure additions bolted onto them (as shell scripts or Excel spreadsheets on a shared network drive if necessary) because refactoring them into an equally pure solution for the real-world case would take too long.
  - frandroid 3y ago
    Okay but the solution here is to identify and parcel your cases into discrete entities. The article doesn't say "don't accept anything odd", it says "clearly identify what you accept". If you have to accept odd cases, identify them so it's clear what's happening. 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.
- 4ad 3y ago
  > The less out-and-out math used to make a point about programming, the better, I think. Imagine if an electrical engineer said this. Or an aerospace engineer. Or any real engineer.
  - vsnf 3y ago
hyperman1 3y ago
I once got a program that was a never-ending source of bugs. It had huge forms, with fields becoming valid or invalid depending on the state of other fields. Each field had listeners to activate/deactivate controls as needed, but the interactions had become so complex that they were full of tiny mistakes. Each tiny mistake slightly corrupted the state, triggering other mistakes, until the whole thing snowballed out of control. Costly business mistakes followed. 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.
- 4ad 3y ago
  > it was too late to make invalid states unrepresentable 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.
  - chii 3y ago
    > It wasn't, that's exactly what you did 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.
nraynaud 3y ago
Funny, I recently had a client telling me his system was non-refundable, so I didn't handle cancellations in the database, later I discovered that actually the sales channel tends to manually refund orders if the request is less than 1h old. Humans are not ready for perfect information representation.
- 4ad 3y ago
  I would argue that languages are not ready for perfect information representation. Programs explode when presented with minor inconsistencies. And changing the representation in minor way requires rewriting the program. With CUE, we are trying to solve this exact problem.
- pjc50 3y ago
  This sinks so many "business transformation" projects, especially in the public sector. An organization contains explicit knowledge, which is written down in its processes, and tacit knowledge, which isn't, and may not be known to managers! But when converting a business to software the tacit knowledge, critical to the functioning of the business, gets lost.
  - nraynaud 3y ago
    It’s also because developing cancellations cost money, and they don’t like spending, so they “forget” some details.
ykonstant 3y ago
Make invalid states unrepresentable, but take care not to make valid states a huge pain in the ass to represent! 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 the caller must prove that the first argument is in the stated range and provide the proof in the second argument. You can `sorry` out, but then you are not programming with constraints. So you need to balance representability with convenience. 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 and having the monad try to reconcile certificates with requirements, or open a proof block to prove the consistency manually. I want to implement something like this when I get the time, but in any case, be wary of extremes!
weinzierl 3y ago
I think it is fair to say that integral types are pretty common in software across the board. Pascal declared integral types like this: month: 1..12; You could also use this nomenclature for characters: letter: 'A'..'Z'; When I first learned C, I could not believe that it did not support that. I wouldn't not have dreamed that almost half a century later I still don't have this feature back. 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; [1] The old one, I don't know much about Delphi and later developments.
- darthrupert 3y ago
  Nim smells like a modern Pascal sometimes, and it has this feature as well.
- int_19h 3y ago
  Take a look at Ada sometime, it really takes that to eleven. 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;
  - nrr 3y ago
    Conspicuously missing are Ada's arrays, which I feel properly take Pascal's to 11 due to the fact that describing their index bounds need not also prescribe that arrays statically allocate that much storage, as in `type Unsigned_Byte_Array is array (Positive range <>) of Unsigned_Byte`, where `subtype Positive is Integer range 1 .. Integer'Last`. Substitute `Positive` with `Natural` where you like.
- 1899-12-30 3y ago
  One really nice thing about object pascal(and nim I think) is that you can declare enums as array indexes. type TMonth = (mJan = 1, etc); TFooPerMonth = array[TMonth] of integer;
zamalek 3y ago
Ever since coming across this idea I have wondered what a (likely relational) database which deeply embedded these concepts would look like.
- another2another 3y ago
  You can actually get quite some way by adding constraints to columns. NOT NULL, default values and a CHECK constraints on a column can limit random invariance bleeding into the db. 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 https://www.postgresql.org/docs/current/ddl-constraints.html
- DylanSp 3y ago
  I've had some idle thoughts about creating a Postgres extension that would make some of these concepts easy to implement and work with. I modeled a sum type/discriminated union a while back, I was able to make it work with constraints, but it was fairly verbose.
  - pdimitar 3y ago
    Which part was verbose? I feel such an extension will immediately find its audience.
    - DylanSp 3y ago
      Writing out the constraints. The starting point was an admin_notes table to start with, where each note initially had the same fields; we later added different categories of notes, where two of the categories had fields that were only meaningful for that category. What I did was add nullable columns for all of the category-specific fields to the table, with constraints to make the category-specific columns only have values for rows of the appropriate category. The type looked roughly like this (using Rust syntax) [1]: 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, }, } Setting up the constraints took about 30 lines of SQL just for those couple of boolean fields on some of the categories, you can see the details here [2]. 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__Add_Category_Specific_Columns_To_TRB_Admin_Notes.sql#L33-L65 https://github.com/CMSgov/easi-app/blob/main/migrations/V164...
terminatornet 3y ago
one of my favorite talks on this topic, "Making Impossible States Impossible" by Richard Feldman: https://www.youtube.com/watch?v=IcgmSRJHu_8 https://www.youtube.com/watch?v=IcgmSRJHu_8 the talk is Elm lang focused, but the concepts still apply to other languages.
wdroz 3y ago
Similar(identical?) concept with typestate pattern[0] [0] -- https://zerotomastery.io/blog/rust-typestate-patterns/ https://zerotomastery.io/blog/rust-typestate-patterns/
Hackbraten 3y ago
I’m not proficient in Haskell but I feel the article is stopping short of making its point. 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?

103 points by satvikpendem 3y ago

FrankWilhoit 3y ago

Strong typing is like violence: if it isn't solving all your problems, you must just not be using enough of it.

hi-v-rocknroll 3y ago
Forth is tic-tac-toe and dependent typing is global thermonuclear war.
- actionfromafar 3y ago
  It would then seem, the only winning move, is not to play.
  - hi-v-rocknroll 3y ago
    How about a nice game of Go?
    - 0atman 3y ago
      10/10, no notes XD
Leo_Germond 3y ago
I love that, going to reuse that one
- FrankWilhoit 3y ago
  Don't credit me, it's not original, but I don't know the actual source.
  - another2another 3y ago
    First time I heard it, it was about XML. So, quite a while ago.

johann8384 3y ago

I thought this was going to be some political thing about states and congress.

klysm 3y ago

This principle has served me well for a long time, but it’s definitely a trade off space. We want to enforce as many invariants as possible through the type system, but more invariants requires more complexity. Eventually you run into dependent types etc.

Leo_Germond 3y ago
I would say it's a tool with an optimal point that is located along the "heavy use" side. I think it is interesting to think of them as solidifying your specification. As such if your spec is still changing or it is unclear (e.g. first impl draft, example code...), you should use some lightweight types, whereas a public API should have types that encode basically everything your comments can say about the values, operations, and memory representation of the parameters. That would be the point where I would consider that defining my types is "done" and I would consider switching to e.g. moving the functiona around instead (there are lots of hanging fruits in safe by construction approaches, that might not even require types - can't shoot yourself in the foot if I remove the footgun entirely)
thom 3y ago
There’s no shame in just having complex constructors to check some invariants in non-structural ways. At least you still capture and enforce the transition.
- 4ad 3y ago
  That only works if your language is value-oriented, but most existing languages use references and mutation extensively.
  - int_19h 3y ago
    I think that's too broad and somewhat outdated. C++ has const, for example, and you're expected to use it. Java and C# give you final/readonly, and not only that, but immutability is becoming more idiomatic, with the language increasingly encouraging it. For example, in modern C#, record Point(double X, double Y); is immutable, whereas the mutable equivalent is the much more verbose: record Point { public required double X { get; set; } public required double Y { get; set; } } Java goes even further by not even having syntax for mutable records - if you want something like that, you have to write it out as a regular class.

hi-v-rocknroll 3y ago

One of the grossest large codebase anti-pattern is god state objects. One of the worst I've seen had to do with the state of conference call. Depending on the state, zillions of properties were or weren't valid. It was a huge, fucking mess that often allowed invalid states to creep in via edge-cases that led to unrecoverable states.

Animats 3y ago

Classically, this is a problem in hardware logic design. It's desirable that logic circuits not be able to lock up in an invalid state. So having a state machine where invalid states cannot be represented is useful. Hardware without this property tends to need reset buttons.

YorkshireSeason 3y ago
The abstract concept here is liveness, aka "eventually something good will happen". In practise, liveness alone is insufficient because a locked up program/processor is indistinguishable from a very slow program/processor. So you really want bounded liveness, along the lines of "within X time units, something good will happen".

orwin 3y ago

I have a question for the author or anyone smart enough to understand the whole post: 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?

orangeboats 3y ago
The way I understand it, "state" refers to any point in time during the execution of a program. 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.
lmm 3y ago
Do you think "state machines" should be called "data machines"? Why or why not? 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").
- orwin 3y ago
  Very insightful (you and your siblings), thank you all. I think I have a fundamental misunderstanding of what a state is, maybe because I mostly practice responding to external state changes? I don't know, I'll think on that. Thank you again.

masklinn 3y ago

A companion piece to this idea (previously at Oleb’s “making illegal states unrepresentable: https://oleb.net/blog/2018/03/making-illegal-states-unrepresentable/ https://oleb.net/blog/2018/03/making-illegal-states-unrepres...) is “parse, don’t validate”: https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/ https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va... 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-type-safety/ https://lexi-lambda.github.io/blog/2020/11/01/names-are-not-...)

vsnf 3y ago

I'm sympathetic to this concept, and it's one I employ from time to time in the various codebases I own, but the type of person to advocate for this kind of thing is also the kind of person to write stuff like > 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.

hnbad 3y ago
I second this as I find that usually the solution that is the most mathematically pure is usually also the one completely inadequate at handling the complexities of real-world applications and end up having various extremely impure additions bolted onto them (as shell scripts or Excel spreadsheets on a shared network drive if necessary) because refactoring them into an equally pure solution for the real-world case would take too long.
- frandroid 3y ago
  Okay but the solution here is to identify and parcel your cases into discrete entities. The article doesn't say "don't accept anything odd", it says "clearly identify what you accept". If you have to accept odd cases, identify them so it's clear what's happening. 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.
4ad 3y ago
> The less out-and-out math used to make a point about programming, the better, I think. Imagine if an electrical engineer said this. Or an aerospace engineer. Or any real engineer.
- vsnf 3y ago

hyperman1 3y ago

I once got a program that was a never-ending source of bugs. It had huge forms, with fields becoming valid or invalid depending on the state of other fields. Each field had listeners to activate/deactivate controls as needed, but the interactions had become so complex that they were full of tiny mistakes. Each tiny mistake slightly corrupted the state, triggering other mistakes, until the whole thing snowballed out of control. Costly business mistakes followed. 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.

4ad 3y ago
> it was too late to make invalid states unrepresentable 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.
- chii 3y ago
  > It wasn't, that's exactly what you did 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.

nraynaud 3y ago

Funny, I recently had a client telling me his system was non-refundable, so I didn't handle cancellations in the database, later I discovered that actually the sales channel tends to manually refund orders if the request is less than 1h old. Humans are not ready for perfect information representation.

4ad 3y ago
I would argue that languages are not ready for perfect information representation. Programs explode when presented with minor inconsistencies. And changing the representation in minor way requires rewriting the program. With CUE, we are trying to solve this exact problem.
pjc50 3y ago
This sinks so many "business transformation" projects, especially in the public sector. An organization contains explicit knowledge, which is written down in its processes, and tacit knowledge, which isn't, and may not be known to managers! But when converting a business to software the tacit knowledge, critical to the functioning of the business, gets lost.
- nraynaud 3y ago
  It’s also because developing cancellations cost money, and they don’t like spending, so they “forget” some details.

ykonstant 3y ago

Make invalid states unrepresentable, but take care not to make valid states a huge pain in the ass to represent! 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 the caller must prove that the first argument is in the stated range and provide the proof in the second argument. You can `sorry` out, but then you are not programming with constraints. So you need to balance representability with convenience. 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 and having the monad try to reconcile certificates with requirements, or open a proof block to prove the consistency manually. I want to implement something like this when I get the time, but in any case, be wary of extremes!

weinzierl 3y ago

I think it is fair to say that integral types are pretty common in software across the board. Pascal declared integral types like this: month: 1..12; You could also use this nomenclature for characters: letter: 'A'..'Z'; When I first learned C, I could not believe that it did not support that. I wouldn't not have dreamed that almost half a century later I still don't have this feature back. 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; [1] The old one, I don't know much about Delphi and later developments.

darthrupert 3y ago
Nim smells like a modern Pascal sometimes, and it has this feature as well.
int_19h 3y ago
Take a look at Ada sometime, it really takes that to eleven. 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;
- nrr 3y ago
  Conspicuously missing are Ada's arrays, which I feel properly take Pascal's to 11 due to the fact that describing their index bounds need not also prescribe that arrays statically allocate that much storage, as in `type Unsigned_Byte_Array is array (Positive range <>) of Unsigned_Byte`, where `subtype Positive is Integer range 1 .. Integer'Last`. Substitute `Positive` with `Natural` where you like.
1899-12-30 3y ago
One really nice thing about object pascal(and nim I think) is that you can declare enums as array indexes. type TMonth = (mJan = 1, etc); TFooPerMonth = array[TMonth] of integer;

zamalek 3y ago

Ever since coming across this idea I have wondered what a (likely relational) database which deeply embedded these concepts would look like.

another2another 3y ago
You can actually get quite some way by adding constraints to columns. NOT NULL, default values and a CHECK constraints on a column can limit random invariance bleeding into the db. 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 https://www.postgresql.org/docs/current/ddl-constraints.html
DylanSp 3y ago
I've had some idle thoughts about creating a Postgres extension that would make some of these concepts easy to implement and work with. I modeled a sum type/discriminated union a while back, I was able to make it work with constraints, but it was fairly verbose.
- pdimitar 3y ago
  Which part was verbose? I feel such an extension will immediately find its audience.
  - DylanSp 3y ago
    Writing out the constraints. The starting point was an admin_notes table to start with, where each note initially had the same fields; we later added different categories of notes, where two of the categories had fields that were only meaningful for that category. What I did was add nullable columns for all of the category-specific fields to the table, with constraints to make the category-specific columns only have values for rows of the appropriate category. The type looked roughly like this (using Rust syntax) [1]: 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, }, } Setting up the constraints took about 30 lines of SQL just for those couple of boolean fields on some of the categories, you can see the details here [2]. 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__Add_Category_Specific_Columns_To_TRB_Admin_Notes.sql#L33-L65 https://github.com/CMSgov/easi-app/blob/main/migrations/V164...

terminatornet 3y ago

one of my favorite talks on this topic, "Making Impossible States Impossible" by Richard Feldman: https://www.youtube.com/watch?v=IcgmSRJHu_8 https://www.youtube.com/watch?v=IcgmSRJHu_8 the talk is Elm lang focused, but the concepts still apply to other languages.

wdroz 3y ago

Similar(identical?) concept with typestate pattern[0] [0] -- https://zerotomastery.io/blog/rust-typestate-patterns/ https://zerotomastery.io/blog/rust-typestate-patterns/

Hackbraten 3y ago

I’m not proficient in Haskell but I feel the article is stopping short of making its point. 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?