Idris Python 发布，希望大家能够参与开发，用类型安全的 idris 写上 Python

项目地址: https://github.com/thautwarm/idris-python

idris 可以让你的程序即证明。也就是可以达到编译过了程序一定正确的程度(如果你不搞可能存在正确性问题的 type coerce

http://docs.idris-lang.org/en/latest/tutorial/theorems.html

依赖类型的好处不仅仅是安全(比如静态越界问题的安全证明)，它还可以帮忙推导参数。比方说我矩阵相乘，类型为 T, MN 的矩阵和类型为 T, NK 的矩阵可以导出一个类型为 T, M*N 的矩阵，而这些维数经常会作为操作函数的参数，比如 numoy, pytorch 的 resize 方法等，这样就可以自动帮你补参数。

机器学习模型组件之间的组合总是要你显式给出一些输入输出的维数，实际上你知道他们之间有些有强耦合性，但你还是得 repeat yourself。Idris 提供给你一个不用当复读机的机会，当然，需要你把对应的 python 库封装好到 idris 侧。

当然，idris 还存在很多使用上不便的地方。这里只是提供一个 make sense 的机会。