That said, I would love to have good data science library support (bindings to stuff like BLAS/LAPACK, Torch, Stan, etc) in Idris.

Imagine vector and matrix dimensions checked at compile time. Probabilities guaranteed to be between 0 and 1, checked at compile time. Compile-time enforcement that you are handling "nil/null" data inputs correctly when reading data from a database or CSV file. Writing a web scraper with linear types to help catch bugs & performance leaks. Maybe even proving theorems about the math code you're writing ("is this a valid way to express X"?).

Maybe not ideal for rapid exploratory model development, but it'd be pretty damn cool for writing data science tooling/libraries and "production" ML code in my opinion.