For the most part I feel that for 99% of problems types just “get in my way”.
It feels like I already know what is going to go in where, and having to type it is just a waste of time.
That said, when I have to work with APIs that can not guarantee their data integrity throwing in a quick @flow annotation of top of the file, and taking the time to write out what is optional has proven very valuable to make sure my functions, and subsequent code is not going to throw.
Another reason I like flow more is because I don’t need to convonce my team to use it, I can just use it myself, and then delete it after I am done writing my code.
I think what you're talking about here is static types getting in your way, not just types getting in your way.
Strong/weak types and dynamic/static types are really two different spectrums. People conflate strong types with static types and weak types with dynamic types, but they aren't really the same thing.
Static/dynamic just has to do with whether the types are checked at compile time or run time. Examples: Static: C, Haskell. Dynamic: Javascript, Python.
Weak/strong has to do with what kinds of checks the type system does. A strong type system is capable of checking a lot of different things for you. Static types are often stronger, but not always: for example, C is statically typed but its type system checks hardly anything: int* + int is perfectly valid. A list of programming languages from weakest-typed to strongest-typed might look something like: JavaScript, C, C++, Common Lisp, Perl, Scheme, Ruby, Python, Java, C#, OCaml, Haskell.
Static types are nice for projects which will grow large and where bugs are a big problem, but I think for the average HN person, static types aren't really necessary.
Strong types, on the other hand, are extremely useful. Even in a dynamically typed language, they aid in debugging a lot, because type errors occur much closer to where they're caused. In Python, for example, `"foo" + 42` immediately fails. But in JavaScript, you don't get an error until much later, perhaps when your webpage is mysteriously displaying "foo42".
Of course, there's a small cost to strong types: in the case where I actually do want to append a number to a string, I have to do `"foo" + str(42)`. But I think people tend to overstate this cost because it's visible. But if you look at the big picture, typing five extra characters takes a lot less time than debugging almost anything.
Also, among statically typed languages there is a significant difference between languages which make the programmer write out all the types and languages which offer type inference. I think most of the comments about types "getting in the way" come from experience with the former (C, C++, Java, C#). In a strongly- and statically-typed language with type inference (such as Haskell) even moderately complex programs can be written without any type annotations. The result looks a lot like a dynamically-typed program, but static types are still inferred and checked for consistency at compile-time. For example, this is a perfectly valid Haskell program:
import Control.Monad
import Control.Monad.Tardis
import System.Random
-- A solution for the Trapping Rain Water problem employing
-- the bidirectional state ("Tardis") monad.
-- https://www.geeksforgeeks.org/trapping-rain-water/
volume hs = sum . flip evalTardis (0, 0) . flip traverse hs $ \h -> do
x <- min <$> getPast <*> getFuture
modifyForwards (max h)
modifyBackwards (max h)
pure (max 0 (x - h))
main = replicateM_ 20 $ do
n <- randomRIO (3, 10)
hs <- replicateM n $ randomRIO (0, 10 :: Integer)
putStrLn $ show hs ++ " => " ++ show (volume hs)
Note that the only explicit type in the entire program is the `:: Integer` annotation on the upper bound for randomRIO. Without that annotation the program would be underconstrained, since the input to `volume` can a list of any type with Ord and Num instances.
Strong/weak is generally not a useful distinction because it has no formal meaning. What you're probably after is "expressiveness" and "soundness". So C's type system is unsound and it's types are inexpressive. Haskell's type system is sound and moderately expressive. Agda's type system is sound and expressive.
> Strong/weak is generally not a useful distinction because it has no formal meaning.
"This doesn't have a formal meaning, therefore it's not useful" is quite a logical leap you've got there.
I've got over a decade of professional programming experience in which "strong types" is a useful enough concept to help me do my job. "Soundness" certainly gives stronger guarantees, but it's more than I've needed.
I'm not aware of "expressiveness" having a formal meaning, but my informal definition has functioned for me so far.
> "This doesn't have a formal meaning, therefore it's not useful" is quite a logical leap you've got there.
It means that everyone defines strong and weak in their own way, which has happened in every type system debate I've seen over the past 15 years.
> "Soundness" certainly gives stronger guarantees, but it's more than I've needed.
Soundness is exactly the metric you need. Either you can rely on your type system not to lie to you, or you can't.
Programming language expressiveness means "Felleisen expressiveness". It's a metric approximated by source code compression, which is why the great programming shootout includes gzip metrics for source programs.
> It means that everyone defines strong and weak in their own way, which has happened in every type system debate I've seen over the past 15 years.
Okay, that's fair. Part of the reason I gave examples and defined the spectrum I was talking about was to address this problem, because I know people don't necessarily know what I'm talking about.
Even static typing very rarely gets in the way (it makes a few programs harder to express; but I find this relevant much less frequently than people think; and even then I’d argue that expressing the types still adds value). What gets in the way, as the video argues, is excessive explicit typing. But languages can get around this with type inference.
I used to feel this way, but the benefits of a good type system far outweigh the drawbacks IMO. A lot of runtime errors caused by dynamic types get pushed back to compile time, which is a much safer and easier time to deal with them. Nowadays writing code without type checking feels like building a house on quicksand.
There's also the self-documenting aspect of strongly typed languages: for instance, if I look up the documentation on a javascript API, I have to hope function parameters have been specified well, otherwise I just have to guess what should be passed in or dig through the source. With a strongly typed language I probably get that information as part of the autocomplete hint.
And good type systems can be powerful tools. In Swift for example, the protocol system is powerful enough that I'm sure it results in writing less code overall, not more.
>But why don't they? Aren't the problems nearly the same? And if not, how?
Concrete example: Common Lisp is very strongly typed. So it almost never automatically converts from type to another, except when it makes total sense (i.e. the square root of -1 will return a complex number).
So, if there is a type mismatch, it will be caught (at runtime) raising an exception. Now, you would think "yeah but my statically typed language will check this BEFORE the code runs". Yes, but in Lisp, the exception doesn't terminate the execution, it enters a mode in which the system asks you what to do next.
Thus, what you do is, you go back to the source code, to the function with the error, you correct that specific function, compile that specific function (which happens almost instantly), and then resume execution of your program. This means that the previously "invalid operation" will be run again but with the new definition of your function, thus the code will continue running without said bug.
Python has the dynamic typing problems, but is better because it has a somewhat strong type system. It will tell you when it's wrong, but often too late (oh this function only gets called wrong once every 100h on my server, thank you for telling me now that it went wrong). And sometimes different types can duck into the same function (e.g. string and list are both iterable).
So yeah, Python suffers from the same issues when you want to scale your code, but it's A LOT less bad than JavaScript.
Don't take this the wrong way, but I suspect you are young developer who hasn't realised that putting in the extra work up front pays large dividends down the line.
Or perhaps there is no correct way to write software and is very dependent on the problem domain and the type of application. I wonder how many projects went over budget, are incredibly over-engineered and ultimately failed because some senior developers read a book on DDD and went crazy with types.
As a side note: The TDD-ish alternative to this, which I also use sometimes is just adding a test where you pass in undefined on your optionals, and then iterating until the test stops throwing.
Unfortunately, “has no obvious bugs” is not quite the same as “obviously has no bugs”. TDD gives you the former, static typing the latter (within what can be represented by the type system, of course)
You have to be willing to use types to express intent. Types are logical propositions, so you have to encode your proposition as a distinct type. You can actually prove many programs correct by exploiting even Java's poor type system:
Type languages, especially static ones, are very inexpressive in the kinds of logical propositions they can express. You can try type hacking (working an inexpressive into more expressive propositions), but the results are often not usable in real systems.
The type language's expressiveness is definitely more limited than the term language, but "very inexpressive" is overstating the case. You end up grouping C, for which your claim is absolutely true, along with Agda for which your claim is not really true.
Regardless, even with Java's limited expressiveness you can encode some powerful propsitions, as the paper I linked shows.
> It may be that COQ and Agda have expressive type systems, but who is writing programs with them? They are not general purpose.
I think that's overstating it a little too. You don't have to use the dependent types, at their core, Coq and Agda are still functional languages and you can just stick to algebraic sums and products and still enjoy type inference. Most people aren't using these languages for general purpose programming because a) poor tooling, and b) because they are explicitly marketed as research languages.
Okay, can you say how you would reasonably catch the typo in my second example with types?
Obviously you have to be willing to use types to express intent, but even if you're willing, types are limited in what kinds of intent they can express.
int* increment(int* i, int step)
{
return i + step;
}
I think your example is flawed. The real problem here is that you're allowed to add an int to an int* with +. int* is not be of type int, and should therefore require some sort of cast to make it possible to add an int to it. Either that, or require a different operator/function to add to a pointer, e.g.:
int* increment(int* i, int step)
{
return prt_add(i, step);
}
Not all type systems are equal, and how the type system interacts with the language is important.
def test_increment(x):
assertEqual(increment(x), x - 1)
The answer to your question is, you can't. In this case the implementation is the specification. You're going to have to set a more meaningful challenge.
Ideally, it's like double-entry book keeping. If you try to express the same thing in two different places, ideally in two different ways, you're less likely to make the same mistake in both places than to make any mistake in the first place. This applies both to types and tests.
def test_increment(x):
assertEqual(increment(x), x - 1)
This isn't a trick question. You run the test, and see that it fails.
If you write the wrong test or the wrong type AND the wrong implementation, they won't help you, but the point of both types and tests is that you have to make two mistakes for a bug to get into production. It's possible that in your test, I could have made the same error in the implementation of `increment`, but it's a great deal less likely than making that error in just the implementation or just the test.
And to be clear, I'm not saying any of this as a "types versus unit tests" thing. I've specifically said that both are useful and needed for reliable software.
> The answer to your question is, you can't. In this case the implementation is the specification. You're going to have to set a more meaningful challenge.
You totally can catch this bug with some type systems (Coq, for example), it's just much easier to catch this bug with a unit test in most languages.
I think that your boss would probably disagree with you that this bug is not meaningful if it makes it into production. You don't get to pick and choose which bugs are meaningful because they don't support your views.
My point is, when the program is the same as the specification then there's essentially no point writing either tests or proofs. Therefore, I think your point would be better demonstrated using a more complicated example.
This is getting a bit off topic and into the theory of how you write tests, but if you wrote a better test it wouldn't be the same as the specification.
I won't paste the full test here because this is part of a larger function, but rest assured I'm not duplicating the definition of the function in the test.
The intern who wrote the code didn't know how to use mocks to mock out `today` so they didn't write a test, resulting in this bug. I remember this case because I use it as an example to teach mocks.
I simplified my original example to make it clearer, but I think you'll see that this real-life bug suffers from the same difficulties if you try to verify it with a type system, but is (fairly) easy to test.
EDIT: Actually, the relevant bits of the test were fairly simple (from memory so please excuse errors):
If the context is Haskell, I'd probably user type-level naturals to encode the correct input/output types.
In other contexts without polymorphic types, like with C, I'd wrap the input and output types in custom structs that expose trusted operations. The more minimal the better. It's definitely more cumbersome without polymorphism, but you do what you can for the code that's mission critical.
I know what you asked, and I answered as best I could without further information. The solution ultimately depends on the specific type system. Like I said, with Haskell I'd use type-level naturals to ensure the output type is 1+input type.
In C, my first thought would be to define a static value representing ONE, checked via static_assert, and then the increment function becomes input + ONE.
> Like I said, with Haskell I'd use type-level naturals to ensure the output type is 1+input type.
I'm a bit out of my comfort zone with this one so I may be wrong, but wouldn't that require a lot of coding to define type level naturals for all the possible values of X?
> In C, my first thought would be to define a static value representing ONE, checked via static_assert, and then the increment function becomes input + ONE.
Okay, but do you agree that in this case a unit test would be a better solution?
I'm not saying this as a types versus unit tests sort of thing. I'm saying both are needed tools for writing reliable software.
On the one hand, in GHC you already have type level naturals.
On the other hand, I don't see that they'd actually be useful for catching this error in any way people are likely to use, although I'd be interested to see attempts...
On the third hand, the way I'd actually implement this in Haskell is probably `succ`, so typo would be caught during compilation. But of course you can construct alternative examples.
To my mind, types and tests are very much complimentary - ideally tests check that your solution gives correct answers at some points in your domain, while types help make that space more uniform (so if it's correct at some points it's more likely correct at others). There are some practical cases where the types sufficiently constrain things that checking any actual points is redundant, but that's not the common case.
> To my mind, types and tests are very much complimentary - ideally tests check that your solution gives correct answers at some points in your domain, while types help make that space more uniform (so if it's correct at some points it's more likely correct at others). There are some practical cases where the types sufficiently constrain things that checking any actual points is redundant, but that's not the common case.
Yeah, this is my ultimate point, and I worry that some people have misunderstood my intent. I'm not criticizing types: I think they're a very important tool. I'm saying that types don't handle every kind of possible error. And conveniently, tests often cover the kinds of errors that types don't (and vice versa).
> I'm a bit out of my comfort zone with this one so I may be wrong, but wouldn't that require a lot of coding to define type level naturals for all the possible values of X?
Not for your simple example. See [1] for more info. There are a number of packages that do the work for you.
> Okay, but do you agree that in this case a unit test would be a better solution?
Depends how mission critical the property is. Even simple increments and offsets might deserve some type-level encoding if they are core, mission critical properties.
For other things, tests are fine, although I recommend property-based testing frameworks like QuickCheck, Hypothesis, etc. which test logical properties against a large range of input values instead of a static set of values encoded into your tests.
It feels like I already know what is going to go in where, and having to type it is just a waste of time.
That said, when I have to work with APIs that can not guarantee their data integrity throwing in a quick @flow annotation of top of the file, and taking the time to write out what is optional has proven very valuable to make sure my functions, and subsequent code is not going to throw.
Another reason I like flow more is because I don’t need to convonce my team to use it, I can just use it myself, and then delete it after I am done writing my code.