The small amount of scientific study around what type checking and static typing gives you is that you avoid around 3% of bugs but even those 3% are easier to fix than the effort in writing them correctly in the first place. While I agree that the subject needs more study but what we know now: the real win would be to have a dev process that lowers criticality of failure (like TDD, CI and other Agile processes) and dispense with static typing for most projects.
Maybe I need to spend some time in Haskell and come over to your way of seeing it. But the studies show that constructing the type system for your problem is very difficult and remains error prone. People routinely make mistakes with types systems of all kinds. I've found I spend more time making the compiler happy that it does making me happy.
But still, my point stands - writing tests during early experimentation is a lot harder than just altering some type and letting the compiler infere what needs to be done or what you broke.
I've spent some time writing Clojure and still use dynamic languages a lot for smaller tasks, so I know both sides. This doesn't mean much, but I'd really encourage you to try some ML language and spend some time with a nice type system. Haskell is probably too big a time investment, so maybe try Elm [0] - it's very beginner friendly and a lot of the people using it come from JavaScript.
With property based testing, your system will come up with mock data for you.
Wow, then you are extremely lucky because bugs like that would occasionally consume a whole day of senior developer time at my previous Python job.
It seems like a symptom of other problems more than anything, and using a staticly typed language will just make those problems manifest in a different way.
If you are writing all of your code from scratch, then it doesn't happen too often. You usually have enough of the current context in your head to avoid most type level mistakes.
The real strengths come from two situations.
The first is refactoring. There is just no contest here. Having every single place where your change affects the test of the program identified automatically is extremely useful.
The second is returning to old code and either trying to understand it or make small changes to it.
http://games.greggman.com/game/dynamic-typing-static-typing/
For an example of a project which I worked on for months, given N molecular graphs, find the maximum common subgraph which is in at least M of them. I did all that in Python. I don't think static types would have made a difference.
Matrix algorithms are an even more clear example. They work with a single numeric type, in a 1D vector or 2D array. It's hard to confuse the types. On the other hand, it's easy to get the algorithms wrong, and choosing the right algorithm can require a lot of design space exploration.
Just think of the number of clustering algorithms available which you might want to try out through prototyping before spending the time to scale things up. How does static typing really help there?
reduceGraph :: Graph a -> Graph Reduced
Even with no knowledge of the problem space, I can think of a whole bunch of static types off the top of my head.
You've already given your input type: N molecular graphs, and a number M.
You've also given your output type: the maximum common subgraph which is in at least M of the given N molecular graphs.
Straight away I can spot a problem with this, since there are no programs of this type. In particular, there is no valid output when M > N. Hence I would refine the input type to ensure that M <= N.
Since it appears in your input type, it would be useful to have a type for "molecular graph". Likewise, based on your output type, it would probably be useful to have types for "subgraph of g", "common subgraph of gs", "maximum common subgraph of gs" and "subset of gs".
Naively, I'd give your program a type something like this:
(m : Nat, gs : Set MolecularGraph, m <= size gs) -> (hs : SubSet gs, size hs >= m, MaximumCommonSubgraph hs)
Whether it would be more or less appropriate for your situation is, of course, an entirely separate issue ;)
[0] In some languages, like older versions of pascal, arrays of different lengths were different types, which was a horror for writing generic code.
Beyond strong typing, do you get the sense that static typing significantly improve prototyping ability for matrix analysis code?
Why shouldn't I be able to do this on a meta-level? There does not appear to be any restriction on, for example, Lisp code regarding the use of problem solvers and provers. The same should go for other metalanguages (perhaps even better, without forcing me into specific semantics).
(Likewise, generative solutions might reduce this problem simply by performing a sequence of correctness-preserving transformations from a higher-level specification. That would shift the burden to checking the specification, which would require a custom checker anyway. Haskell's capability to check or automatically derive stuff seemed limited the last time I looked at it.)
Also, using a type checker to wholly check your Lisp code basically makes it a static language, the difference then is pretty much philosophical I'd say.
I'd rather avoid someone forcing me into using a hardcoded type system, among other reasons because I'm contemplating a (perhaps novel?) search-based program/expression-manipulating system that wouldn't play well with any fixed typing system. For one thing, the types of expression results (being return values of operators applied to input expressions or programs) can easily be emergent (is the resulting expression linear? Is it an odd function? Is it analytically integrable? Etc.) and not easily arrived at in something ML-like. If I had to use something like Haskell, I'd still be rolling out my own type system/prover on top of the existing language implementation anyway. However, types in general (as something you can compute with in the meta-program) would be absolutely mandatory for a system like this (for example, some algorithms or operations can have more desirable refinements that work only on subsets of values - consider determinants of triangular matrices, with triangular matrices being an emergent type - and I absolutely want to find out if such a thing is available for the specific problem being transformed), just not types that any specific existing language offers, to my knowledge.
So it's not that I dismiss the notion of proving things about programs - that is a vital thing to have - but the ability to impose restrictions on a program from the outside seems much more flexible to me than going for some fixed type discipline that could force me to straddle inconvenient fixed walls in the structure of a complicated program (such as this transformation system that would search the tree of possible transformations for a result with some desirable properties, with the transformations concisely expressed in some very-high-level DSL source code).
If instead of having separate Person and Address types you just use strings for everything (even "lists" can be strings - just keep the data serialized into HTML, or XML) then you can your program is likely to "do something" if you just compose a bunch of functions together. Sure, your code might have a bunch of logic bugs (like HTML injection / XSS) but at least it does something!
Static typing is great once you leave this "stringly typed" world and start separating your values into strongly-typed types. When you get a type error from passing a value to the function then its nice if you can be warned about this at compilation time.
How? By building the structure/hard stuff first and letting the compiler verify it while leaving out the uninteresting parts.
A very simple example. Let's say you have some data model with people, addresses, whatever. You want to see what you need to do to get a list of addresses for some group of people.
You start by defining the structure of your data model (this can depend on DB schema, business requirements, whatever):
Now, go straight to the hard part. No need to fuck around with DB connections, mock data, whatever: Leave out the implementation for now. So probably we are gonna need a way to get an Address for a Person. Ok: Again, leave out the implementation. Now go back to `getAddresses` and see if we can implement it now: Cool, the compiler doesn't complain. So far we've verified that if we have a function like `addressForPerson` we can safely assume that our design is going to work.Now we can go back to `addressForPerson` and implement that. But turns out, we only have a city stored in Person, so the best we can do is get back a list of potential addresses for each person. So we need to adjust that type signature:
Leave out implementation, it's trivial so no need to spend time on it now. But now the compiler complains that `getAddresses` doesn't make sense anymore! We are saying that, having a list of people, we can get a list of addresses, but that's not true anymore. We found out that we can only get a list of potential addresses, so we have to adjust the type signature. Now every use of `getAddresses` will have to be adjusted to the new requirements. Etc etc.Granted, this is a very simple example, but I hope it illustrates how static languages facilitate extremely fast prototyping. Sure, a Lisp REPL is very very nice, but in my personal experience it's no match for a type system. We didn't even have to mock data to start experimenting!
(And yes, Haskell, OCaml, PureScript, Elm etc all have a REPL too).