3 ms·
> The point of typing is to move errors to compile-time. You've got to understand: Whether or not a particular email address is verified or not isn't something
by jmull 4y ago
> The point of typing is to move errors to compile-time.
You've got to understand: Whether or not a particular email address is verified or not isn't something that's generally known at compile time... That means compile time checks cannot actually guarantee if that email address is verified or not.
The compiler cannot know something that isn't known. There must be runtime code somewhere doing the check.
What people are really talking about with types here is that if you organize your code in a certain way, you can put the code that verifies whether an email address is verified or not in one place and use types to help make sure other code doesn't accidentally ignore or change that guarantee.
That's good and fine. But... (1) you can do the very same thing without types; (2) Either mechanism is only as good as your code organization and controls that ensure there's a single place this is determined (and that that place is correct).
- hither_shores 4y ago> Whether or not a particular email address is verified or not isn't something that's generally known at compile time Yes, obviously. What is knowable at compile time is the stuff that comes after: given that the input to this function has property X, does the output have property Y? Arguments, not premises. > But... (1) you can do the very same thing without types Sure, and if someone makes an SMT-solver-oriented language (that isn't just using it to drive type inference) I'll be happy to try it out. But what most people who dislike types claim is that you can replace them with testing (true in principle, false in practice: no one actually remembers to test every last edge case every single time) or just programmer discipline (lol).
- jmull 4y agoI like types just fine. They are great for expressing static constraints.