Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The type system is a programmer's best friend

dusted.codes

Post reply on HN
Print view View original

61–70 of 467 posts

Re: The type system is a programmer's best friend

#61

Post by dwheeler »

cardanome wrote: post #52

Oh god, please just use primitive types. Don't make assumptions about things. Everyone thinks they are so smart validating emails, phone numbers, zip codes and all until their great design goes live and they discover that users in the real world do not follow their assumptions. I have seen that happen again and again. No, if your idea of validating an email is more complicated than "should have an @ symbol", I guaran…

Using specialized types can be useful, but if it provide s methods they need to be correct for ALL situations.

Here's a subversion of GitHub's authentication (now fixed) where they assumed that "lowercasing domain name using English case rules is always fine and produces the same result" led to a vulnerability: https://dev.to/jagracey/hacking-github-s-auth-with-unicode-s...

Re: The type system is a programmer's best friend

#62

Post by hansvm »

cardanome wrote: post #52

Oh god, please just use primitive types. Don't make assumptions about things. Everyone thinks they are so smart validating emails, phone numbers, zip codes and all until their great design goes live and they discover that users in the real world do not follow their assumptions. I have seen that happen again and again. No, if your idea of validating an email is more complicated than "should have an @ symbol", I guaran…

That sounds like an argument against excess validation rather than against types (maybe because of blog-driven development showing minimal examples of the power of types?).

Picking on one of those points, suppose emails are just strings. What then prevents them from getting used as names, identifiers, and other unrelated data? Just your continued vigilance as a programmer and hoping that nobody ever carelessly names the field "address" so that mistakes can slip by over a series of devolution commits.

You might not know much about what an email is, but you know _something_ about how you expect them to behave and be used, and if you like the computer to automate your work it's not totally unreasonable to rebind the string type as an email type and require explicit conversions at the point of use to treat it as anything other than just an email. There's zero runtime cost, it's not much more code, and that class of bugs is greatly reduced except for at the boundaries of the system.

Maybe that effort isn't worth it, or maybe your domain changes fast enough you'd have a lot of churn, or maybe those bugs aren't too important, or whatever. Using types to help you reason about the things you do know and do care about can be a huge productivity boost though, so I wouldn't just write the whole technique off.

Re: The type system is a programmer's best friend

#63

Post by leephillips »

mdm12 wrote: post #36
mikewarot wrote: post #3

I once attended a meeting where a Professor from a University somewhere in Chicago gave a brilliant demonstration of using a similar type system for dealing with values in Electrical Engineering. It made quite sure you couldn't do things like add volts and amps. [Edit] it also handled things like parallel resistances, etc. It was in C++ if I recall correctly. This is a great idea, that I've haven't had cause to use y…

Unit of measures are a great example of what a type system can do, and something not enough languages support. F#[1] and Scala[2] are two that I know of that do support UOMs. Like you, I haven't had the need to use them in the domains I work in, but I imagine that they would be invaluable in certain contexts. [1] https://learn.microsoft.com/en-us/dotnet/fsharp/language-ref... [2] https://github.com/typelevel/squants

Julia has this via a package: Measurements.jl.

Re: The type system is a programmer's best friend

#64

Post by pfdietz »

djha-skin wrote: post #40

The most successful languages are typed but weakly so. Just enough type system to avoid the biggest class of bugs, not enough to get in your way all the time. Golang strikes this balance very well. Too little typing, and your Python unit tests get too heavy to run after every commit. Too much, and you have to read a book on category theory before you can figure out how to grab that one field using Lenses in Haskel. E…

I want to point out that in practice, Common Lisp is also to some extent statically typed. The compiler will issue warnings if there are forms that it can determine (at compile time) would cause type errors at runtime. It's common practice to not accept code unless these errors are eliminated (one can even set up your compile system to abort when they are found.)

What it will not do is reject the program unless it can confirm that every expression will not cause a type error.

Re: The type system is a programmer's best friend

#65

Post by Spivak »

an1sotropy wrote: post #50
Smaug123 wrote: post #11

Earlier quoted context omitted.

2000 square dollars? If I'm choosing between ways to spend capital so as to improve the efficiency of a process, and that process currently produces five widgets per dollar, then the quantity I'm comparing to choose between my courses of action can be measured in widgets per square dollar. Hiring a better engineer for more money may create an efficiency improvement of 1 widget per dollar, with an outlay of $1k extra…

Is this getting downvoted? bummer. You have provided a real example, which I was looking for, of why one might need to express a square dollar; thanks. I wonder if the people who want to argue "types save you from bugs" see your example as very unwelcome, since they'd want to use "squared dollars" as an example of something nonsensical that should be flagged as a type error. I hope those people can reflect rationally…

But it shouldn’t be an error in any unit system.

   # oops my scaler has a unit
   x unit * x unit = x unit^2
The value isn’t catching this line of code since it’s potentially valid. It’s catching the line of code where you pass the result to a function that expects unit.

Re: The type system is a programmer's best friend

#66

Post by docandrew »

mdm12 wrote: post #36
mikewarot wrote: post #3

I once attended a meeting where a Professor from a University somewhere in Chicago gave a brilliant demonstration of using a similar type system for dealing with values in Electrical Engineering. It made quite sure you couldn't do things like add volts and amps. [Edit] it also handled things like parallel resistances, etc. It was in C++ if I recall correctly. This is a great idea, that I've haven't had cause to use y…

Unit of measures are a great example of what a type system can do, and something not enough languages support. F#[1] and Scala[2] are two that I know of that do support UOMs. Like you, I haven't had the need to use them in the domains I work in, but I imagine that they would be invaluable in certain contexts. [1] https://learn.microsoft.com/en-us/dotnet/fsharp/language-ref... [2] https://github.com/typelevel/squants

Packages exist for Ada, too: http://archive.adaic.com/tools/CKWG/Dimension/Physical_units...

Re: The type system is a programmer's best friend

#67

Post by RHSeeger »

cardanome wrote: post #52

Oh god, please just use primitive types. Don't make assumptions about things. Everyone thinks they are so smart validating emails, phone numbers, zip codes and all until their great design goes live and they discover that users in the real world do not follow their assumptions. I have seen that happen again and again. No, if your idea of validating an email is more complicated than "should have an @ symbol", I guaran…

Just because there are cases where over-validation (email address being the primary example) can be a problem doesn't mean that _no_ type validation is useful. There are many, many places where validation-beyond-primitives is useful, or even just types that need actions taken on them before they can be used in place of another type. One simple one is "non-negative integers", not commonly provided as a primitive type but _very_ common to need to be able enforce. Complex numbers are another. Normal strings vs HTML strings (need to be properly handled before they can be output to a front end). The list is endless, and custom types can provide a _lot_ of safety.

Re: The type system is a programmer's best friend

#68

Post by shaboinkin »

I'm working in a codebase that has, at times, 10+ different expressions within a single conditional in many places, and trying to pull out the context of why the conditional exists in the first place make grug brain hurt. At the very least, you could put all of the expressions and assign to a boolean with a variable name saying wtf it is you're conditioning on.

https://grugbrain.dev/#grug-on-expression-complexity

Re: The type system is a programmer's best friend

#69

Post by throwawaymaths »

mdm12 wrote: post #36
mikewarot wrote: post #3

I once attended a meeting where a Professor from a University somewhere in Chicago gave a brilliant demonstration of using a similar type system for dealing with values in Electrical Engineering. It made quite sure you couldn't do things like add volts and amps. [Edit] it also handled things like parallel resistances, etc. It was in C++ if I recall correctly. This is a great idea, that I've haven't had cause to use y…

Unit of measures are a great example of what a type system can do, and something not enough languages support. F#[1] and Scala[2] are two that I know of that do support UOMs. Like you, I haven't had the need to use them in the domains I work in, but I imagine that they would be invaluable in certain contexts. [1] https://learn.microsoft.com/en-us/dotnet/fsharp/language-ref... [2] https://github.com/typelevel/squants

It's also something that some languages seriously screw up. Consider multiplying a time (which is typed in go) with a numerical value... suppose what I want is a user to input number of time intervals to wait. So the user wants 5, and the interval is 2500 milliseconds. The way you get 12500 milliseconds out of that made me want to throw my computer out the window.

Re: The type system is a programmer's best friend

#70

Post by docandrew »

I have to plug Ada's rich type system for explicitly encouraging this kind of design. With things like type predicates [1], you can do run-time enforcement or even prove at compile-time (to optimize away the runtime checks) that type constraints are met.

As an example of this, in a piece of code I'm working on there's a Base64_String type, where only RFC 4648 characters are permitted to be part of the string, the '=' padding character can only appear at the end of the string, and if the second-to-last padding byte is '=' then the last one must be as well. This is all enforced by the type system without having to call "validate()" or something every time its used.

1. https://learn.adacore.com/courses/intro-to-ada/chapters/cont...

Post reply on HN