# IdrisLearning

### Premise

Modern ML tools, like Tensorflow and PyTorch, are not production-ready.

1. They were created as experimental tools and were further used and updated due to extreme speed of the DL field development only.

2. Those frameworks were mostly developed by interns and Google Summer of Code students. Now they are maintained by a dedicated teams, but multiple design flaws, like inconsistent interfaces, still stick out.

3. Absolute majority of those frameworks are based on an inappropriate base: Python - a script language with weak dynamic typing, which contradicts with a declarative nature of DL model engineering. Even external tools like static type checkers hardly solve the problem. At the same time, DL naturally appeals to static V&V - tensor shapes may be inferred at compile time and shape conformance of the whole computation graph may be validated. In reality, a very common scenario is a Python program failure because of dimensions mismatch. A lot of computational resources and time may be wasted in case of such collapse.

4. Python is well-known due to its performance and multi-threading issues. Industry-level performance may only be acquired by using bindings to low-level libraries written in C.

### Proposal

We propose a project of constructing a data science ecosystem, based on a compiled, statically typed base of Idris.

It would resolve many runtime problems of a modern DS mega-framework just because Idris is statically typed and has a notion of dependent types.

It would also be a better product from SE point of view because requirements to DS tools and everyday DS processes are much clearer than they were 5-7 years ago, when TF and PT projects were started.

### Roadmap

At the beginning, we plan to utilize modern frameworks and see first phase of our project as a translator to TensorFlow and\or PyTorch. Static checks are applied while most of the current pipeline is preserved.

As the development continues, we plan to descending in the target abstraction level - compiling directly into CUDA and BLAS, eventually moving to assembly code generation.

The resulting product assumes to be better than its counterparts on every step of development starting from MVP - solving existing problems while introducing little to no of its own.

The project may also lead to a number of publications or papers, which we would be happy to write.