首页   注册   登录
V2EX = way to explore
V2EX 是一个关于分享和探索的地方
现在注册
已注册用户请  登录
推荐学习书目
Learn Python the Hard Way
Python 学习手册
Python Cookbook
Python 基础教程
Python Sites
PyPI - Python Package Index
http://www.simple-is-better.com/
http://diveintopython.org/toc/index.html
Pocoo
值得关注的项目
PyPy
Celery
Jinja2
Read the Docs
gevent
pyenv
virtualenv
Stackless Python
Beautiful Soup
结巴中文分词
Green Unicorn
Sentry
Shovel
Pyflakes
pytest
Python 编程
pep8 Checker
Styles
PEP 8
Google Python Style Guide
Code Style from The Hitchhiker's Guide
V2EX  ›  Python

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

  •  
  •   thautwarm · 88 天前用 Android 发布 · 617 次点击
    这是一个创建于 88 天前的主题,其中的信息可能已经有所发展或是发生改变。

    项目地址: 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 的机会。

    1 回复  |  直到 2019-04-25 15:58:02 +08:00
        1
    1800x   88 天前   ♥ 1
    started
    我现在用类型注解+pyright
    关于   ·   FAQ   ·   API   ·   我们的愿景   ·   广告投放   ·   感谢   ·   实用小工具   ·   997 人在线   最高记录 5043   ·     Select Language
    创意工作者们的社区
    World is powered by solitude
    VERSION: 3.9.8.3 · 18ms · UTC 18:46 · PVG 02:46 · LAX 11:46 · JFK 14:46
    ♥ Do have faith in what you're doing.