I'm not an expert on type systems, but I don't think it would add that much in your case. You might get more out of it if you wanted by using phantom types, which is just a way to differentiate among structurally identical types, like this:

    reduceGraph :: Graph a -> Graph Reduced

Now you can't pass unreduced graphs to functions where you expect some sort of an already reduced graph, and you could encode as much invariants as you wanted in your types, but yea, in cases where there are homogenous types with little variance (machine learning, statistics, your use case) static typing won't probably bring that much (unless you go nuts with dependant typing I guess).

> 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.

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)

Programming with type constraints like these would be very different to using Python, where you'd have no guarantee that a value is even a graph, let alone a maximum common subgraph of the input set.

Whether it would be more or less appropriate for your situation is, of course, an entirely separate issue ;)

Matrices and vectors can be thought of as typed by dimension[0], and it's easy to get that wrong. (I want to say c++'s eigen can do some compile-time checks if it has the dimensions available).

[0] In some languages, like older versions of pascal, arrays of different lengths were different types, which was a horror for writing generic code.

Yes, C++ is a particularly easy language to get that wrong, where float * can be a pointer to scalar, vector or 2d array. Other more strongly typed languages, like Python, will make those errors easy to spot with any sort of test case.

Beyond strong typing, do you get the sense that static typing significantly improve prototyping ability for matrix analysis code?