But the nonempty list never has an element, so we don't need to worry about the type mutation of removing an element from it. Filter just returns a nonempty list.
The problem is that user inferring doesn't scale. For small projects this is reasonable but for enterprise software engineering it is easy for a constraint that isn't enforced by the type system to be missed by an engineer leading to a bug. Whereas typed constraints naturally propagate throughout the system.
But then ironically, the problem with relying on programming language type systems is that they don't scale (beyond the boundaries of a single process). As soon as you are crossing a wire you have to go back to runtime validations.
Throwing out type safety simply because you have unverified input is a little silly. It's trivial in most statically typed languages to safely turn input into a concrete type (or an error if it is invalid) at the edge and meanwhile maintain type safety throughout the rest of the code.
There's where good documentation and training pays off.
Some invariants that are too complex to express purely in code, requiring numerous separate low level bookkeeping functions throughout the system, can be concisely expressed as a high level idea in natural language (wether as comments or at an external technical document).
Make sure that your developers are exposed to those documents, throw in a few tests for the most obvious cases to ensure that newcomers are learning the invariants by heart, and if they're competent you should not have problems but in the most obscure cases (that could appear anyway even if you try to formalize everything in code).
I eagerly await your implementation of a type describing my tax return. And to implement a compiler for the new programming language you'll inevitably have to construct, we're gonna need two types, one expressing all valid source programs, and the other all valid programs for the target platform.
Oh, can we also get updates to that for next year's taxes, new platforms, and other such future business needs? Of course the current requirements have to still remain supported.
There is no world where the added time here for the developers is with the trade off, and if you look through my history, you will see that I largely reject “dev time trade off” as a notion a company should ever seriously entertain as a significant burden.
Yeah - in theory they are the same thing. You can have a dependent type that's an array with a length of 5 or you can create a type called ArrayLengthFive, and in both cases the type checker ensures that you don't accidentally use an unbounded array.
But the difference is that with a dependent type, you get more guarantees (e.g. my ArrayLengthFive type could actually allow for arrays of length 20!). And the type checker forces you to prove the bounds (there could be a bug in my code when I create an ArrayLengthFive). And the dependent type allows other parts of the system to use the type info, whereas ArrayLengthFive is just an opaque type.
I do think there is room for both ways of working. In the string -> Email example, it's probably enough to parse your string and just call it an email. You don't need to try to encode all the rules about an email into the type itself. But there are certainly other cases where it is useful to encode the data constraints into the type so that you can do more operations downstream.
Parsing a string into an email, of course, is already fraught with peril. Is it valid HTML? Or did you mean the email address? Is it a well formed email, or a validated address that you have received correspondence with? How long ago was it validated? Fun spin on the, "It's an older code, sir, but it checks out."
I've seen attempts at solving each of those issues using types. I am not even positive they aren't solvable.
Validation is an event, with it's own discrete type separate from the address itself. This is no different than a physical address.
123 Somewhere Lane
Somewhereville, NY 12345
is a correctly formatted address but is almost certainly not one that physically exists.
Validation that it exists isn't solvable in the type system because, as I mentioned, it is an event. It is only true for the moment it was verified, and that may change at any point in the future, including immediately after verification.
I think I get your point. I would add reconciliation to validation. In that sometimes you cannot validate something without doing it, and are instead storing a possibly out of band reconciliation of result.
I'm curious, though, in how this argument does not apply to many other properties people try and encode into the types? It is one thing if you are only building envelopes and payloads. And, I agree that that gets you a long way. But start building operations on top of the data, and things get a lot more tedious.
It would help to see examples that were not toy problems. Every example I have seen on this is not exactly leaving a good impression.
There are things that can embed a bit of temporal logic into types, such as a linear type that can statically guarantee a file handler has been closed exactly once, or error.
For the most part, what I think people really want are branded types. F# has a nice example of unit, where a float can be branded Fahrenheit or Celsius or Kelvin, and functions can take one of those types as parameters.
You then have some function that can parse user input into a float and brand it one of those types. The compiler doesn't make any guarantees about the user input, only that the resulting branded value cannot be used where a different one is expected. Other good examples are degrees and radians, or imperial and metric, etc.
Depending on what you are doing, knowing at a type level that some number can never be negative (weight in pounds) can save you a lot of hassle. If one part of the system doesn't brand a value, and it feeds into another part of the system that is branded, you're stuck with extraneous runtime checks all over the place or a lot of manual unit tests. Instead, the compiler can point out exactly, and in every instance, where you assumed you had a validated value but instead did not.
Some of these are why I would add reconciliation to the idea. Linear types, specifically. You can encode that you only send a message once. But, without doing reconciliation with the destination, you can not be sure that it was received.
I'm torn, as the examples from small programs make a ton of sense and I largely like them. I just cannot escape that every attempt I've seen at doing these in large programs is often fairly painful. I cannot claim they are more error prone than the ones that skip out on it. I can say they are far more scarce. Such that the main error condition appears to be to stall out on delivery.
> In the string -> Email example, it's probably enough to parse your string and just call it an email. You don't need to try to encode all the rules about an email into the type itself.
There is also the in-between Rust approach. Start with the user input as a byte array. Pass it to a validation function, which returns it encapsulated within a new type.
What is annoying is the boilerplate required. You usually want your new type to behave like a (read-only) version of the original type, and you want some error type with various level of details.
You can macro your way out of most of the boilerplate, with the downside that it quickly becomes a domain specific language.
The salient excerpt is: "A parser is just a function that consumes less-structured input and produces more-structured output". In opposition to a validation function that merely raises an error.
It's a little more impactful than that. Have a look at Z3, Boogie, Dafny, and similar technologies to see practical application of what I mean. It boils down to there being "non-general" algorithms that still work for virtually every input you're ever going to give them. A hypothetical algorithm that decides the halting problem for 99.9999999% of programs would not violate the impossibility proof.
The limit case is maybe interesting. What about the algorithm that decides the halting problem for every program except for one? Does the impossibility proof prohibit such an algorithm? Does it make a difference if the identity of the unique program is known or unknown?
And then of course there is classic pen and paper hand derivation like the old guard (Knuth and his peers) did. The claim that that is following an algorithm is yet to be proved or disproved.
Big fan of todoist. I've been using it for less than a month, but have already switched to the yearly subscription. I use Obsidian for my notes, but for remembering to do something, I now use Todoist. Any passing thought that I want to deliberately go back to (or even patterns of thinking, like every 6 months, reflect on this concept) can be put into Todoist and I know that I'll see it again.
I contemplated trying to do all of this in Obsidian but the conventional advice seems that while you can, it isn't worth it. Todoist offering a simple mobile interface where I can quickly add a task is great. I wish reminders worked a little better (I'd been using alarms on my phone for reminders I want at a specific time, and Todoist reminders aren't nearly as attention grabbing).
I know they offer time-based tasks, but I've never used them. I limit myself to a resolution of one day and then setup alarms in the morning if I need.
I've noticed some streaming platforms have ads for other shows/movies they've made. I don't love these but can tolerate them because:
1. They are only at the start of a show, so I'm not interrupted.
2. They offer a skip button.
3. They are ads for somewhat-relevant content and I don't tend to explore the space of other things to watch very much.
That said, it's a knife-edge for me. If they got even a smidgeon worse I probably wouldn't watch anything on those platforms.
Linking is an exceptionally good idea. It is very transformative to how I think about organizing information and doing it with Obsidian the past few months has felt great. Besides future proofing, I love the speed of processing a simple text format like markdown (plus local first) allows. Everything opens instantly, which feels very different from things like Google docs or Microsoft Word. About the only note tool it doesn't replace for me is spreadsheets that use math. There are plugins but it doesn't feel quite as clean as Google sheets for this purpose.
Does it though? In my experience any "credit" for fair behaviour disappears very fast. Employees don't really care about fairness, they care about themselves here and now.
Equally businesses see employees as disposable, and work to maximise short term profit, not fairness. There's generally a lack of trust in one, or both sides, and that results in poor behaviour from both sides that spirals.
Sure there are great companies to work for, but all their greatness is tossed aside as soon as a better offer comes along. Employees look out for #1. Employers do the same.
People generally like long-term stability and are willing to trade their loyalty in exchange for that, even to the point of turning down a more lucrative offer. Back when companies appreciated that, you had plenty of people with a stable employment at the same company for literally decades. But then this cycle was broken when employers started to treat their employees as disposable (all while still demanding at least token loyalty!) in pursuit of more profits - and they have succeeded in teaching the employees that any talk of loyalty from a business is virtually guaranteed to be a scam, so why would the latter ever take it seriously?
Highly recommend Freya's various deep dives into various game development contents. She also has twitch vods for developing those videos which are also fascinating.
