Comment by klysm
2 years 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.
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)
Invariants need to be encoded one way or another anyway, you can't escape that. If your type system is not sophisticated enough this gets tedious and awkward to do in the type system, so it's easier to do in (dynamic) code. But dependent types simplify this, they make it much easier to express yourself in types compared to, say, all the various fancy extensions to System F. Computing types becomes just like computing terms.
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.
(Assuming ADT here refers to Algebraic Data Types, as opposed to abstract data types)
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"
I forgot about Swift, that's true (and great).
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.
6 replies →
I definitely agree that ADTs are a big step forward; when I learned about them from Haskell, I was kind of baffled that they weren't more common, because the concept of "this value is always either type A or type B" is pretty simple and occurs a lot. I really wish Go had included them, because it doesn't seem like a terribly complex concept, the type switch syntax would work decently for basic pattern matching, and having ADTs built into the ecosystem from the start would be much smoother.
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.
That only works if your language is value-oriented, but most existing languages use references and mutation extensively.
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#,
is immutable, whereas the mutable equivalent is the much more verbose:
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.
1 reply →
I've come out of a job of spaghetti and idiots.
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.