Comment by phplovesong
17 hours ago
You seem to have a fundamental misunderstanding about type systems. Most (the best?) typesystems are erased. This means they only have meaning "on compile time", and makes sure your code is sound and preferrably without UB.
The "its only bits" thing makes no sense in the world of types. In the end its machine code, that humans never (in practice) write or read.
I know, but a type system works by encoding what you want the data to do. Types are a metaphor, and their utility is only as good as how well the metaphor holds.
Within a single computer that’s easy because a single computer is generally well behaved and you’re not going to lose data and so yeah your type assumptions hold.
When you add distribution you cannot make as many assumptions, and as such you encode that into the type with a bunch of optionals. Once you have gotten everything into optionals, you’re effectively doing the same checks you’d be doing with a dynamic language everywhere anyway.
I feel like at that point, the types stop buying you very much, and your code doesn’t end up looking or acting significantly different than the equivalent dynamic code, and at that point I feel like the types are just noise.
I like HM type systems, I have written many applications in Haskell and Rust and F#, so it’s not like I think type systems are bad in general or anything. I just don’t think HM type systems encode this kind of uncertainty nicely.