V2EX = way to explore
V2EX 是一个关于分享和探索的地方
现在注册
已注册用户请  登录
推荐学习书目
Learn Python the Hard Way
Python Sites
PyPI - Python Package Index
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
wcsjtu
V2EX  ›  Python

有没有老哥推荐一个支持 struct 类型的 hindley-milner 实现

  •  
  •   wcsjtu · 106 天前 · 1061 次点击
    这是一个创建于 106 天前的主题,其中的信息可能已经有所发展或是发生改变。

    迫于项目需求, 小弟正在学习类型推导相关的知识。了解到 hindley-milner 是常用的类型推导算法,但是网上找了一圈,都是函数式语言的实现, 小弟想把类型推导用在 Python 上。

    国外有个大神用 Python 实现了 HM 的 demo ,https://github.com/rob-smallshire/hindley-milner-python/blob/master/inference.py 。 但是这个 demo 太简单了。如果要考虑 struct 类型,该怎么实现呢?有没有老哥推荐个,我去参考参考

    12 条回复    2022-10-31 20:21:58 +08:00
    pisc
        1
    pisc  
       106 天前   ❤️ 1
    Type Inference 会用到很多 PL 知识,我觉得你应该先系统地补一下 PL 和 类型系统相关的知识(如果你没太多时间的话,可以简单看一下 http://lucacardelli.name/papers/typesystems.pdf )?没有相关知识的话,感觉会比较吃力 ,你需要看透 Python 那些类型的实质是什么,比如 “struct”, tuple 和 product type 的关系,在 Python 这种语言上做类型系统本来就不是太容易,你可以看看某网红写的 https://github.com/yinwang0/pysonar2 (虽然可能不是你想要的 HM )
    pisc
        2
    pisc  
       106 天前
    可以直接说你的项目需求是什么,可能会比你问 HM 和 struct 之类的(因为这个路径可能是错的),别人更能帮助到你
    Austaras
        3
    Austaras  
       105 天前   ❤️ 1
    虽然不知道你说的 struct 是什么,但目测说的是 row poly ,那其实可以看看 elm 的实现,或者直接搜论文
    wcsjtu
        4
    wcsjtu  
    OP
       105 天前
    @pisc 多谢大佬。我们之前做了一个"Python" ==> C++的 transcompiler 。 但是没有静态检查,导致 Python 代码有问题不能在 Python 层发现, 得编译生成的 C++代码才知道。 没有类型信息,一些 high level 的优化也没办法做。所以想着 HM 能不能解决我的问题。

    这里的"Python"是一个 Python 非常小的子集,只支持非常小部分的语法、类型和标准库。其中类型只有 str/int/float/complex/list/dict/tuple/deque/set 和 `dataclass`。 所以做类型推导应该没那么难.....

    我没有系统学过 PL 方面的知识, 所以想找些 demo ,我去参考一下, 再照着写……
    wcsjtu
        5
    wcsjtu  
    OP
       105 天前
    @Austaras 大佬能给个搜索关键字吗, 我不是 PL 背景出身……行业黑话看不懂啊
    Austaras
        6
    Austaras  
       105 天前
    row polymorphism 就是搜索关键字啊
    secondwtq
        7
    secondwtq  
       105 天前   ❤️ 1
    HM 是常用的算法但不是唯一的。HM 的特点倒是非常明显,标准的 HM 可以在没有任何 type annotation 的情况下推导出一整个程序的 principal type 并且对于大多数实际程序都很快。但是这是类型系统本身做了一些妥协的前提下的(其实 HM 这词本来是指这个类型系统不是推倒算法,那算法叫 Algorithm W )。

    先不说什么 higher-ranked type 的问题,在 ML 等基于 HM 的语言中,取列表 x 的第 y 项需要写成 List.nth x y ,其实这里面这个“List”(准确来说是 List.nth 这个函数的类型)已经告诉算法 x 是某种 list ,y 是个 int 。而如果(以 Python 为例)算法只能拿到一个 x[y],是无法分辨 x 到底是个 list ,还是 tuple ,dict 的,y 的类型也无从确定。再比如说定义俩 struct (虽然 FP 圈一般习惯叫 record )分别叫天猫和京东,每个 struct 有个字段叫双十一,然后 def foo x = x.双十一,x 的类型就喜闻乐见二选一了。这就是为啥 HM 只在部分 FP 语言里吃得开,毕竟大多数常用编程语言都是按照后者的思路设计的,再来点 subtyping 直接跪。

    我的意思是这东西上限也就那样,毕竟就算 FP 语言类型系统沾点高级特性也基本是用不了 HM 的。当然你这个比较简单拿 HM 来魔改一通大概是勉强能行的,我上面提的问题用 Typeclass ,Row Polymorphism 之类常见扩展也都能解决,不过可能会搞得实现和类型签名稍微复杂一点。不过检查个正确性貌似也并不需要 care 类型签名 ...
    wcsjtu
        8
    wcsjtu  
    OP
       105 天前
    @Austaras 多谢大佬,我去学习下什么是 row polymorphism
    wcsjtu
        9
    wcsjtu  
    OP
       105 天前
    @secondwtq 多谢大佬。

    1. 我理解,像

    ```python
    def foo(x):
    y = x.双十一
    ```
    这样的代码, 确实推断不出来 y 的类型。但是如果有上下文,或者有类型标注, 应该还是推出来吧。

    2 . 我理解`x.y`和`x[y]`应该是比较类似的, 如果知道了 x 的类型, 那么`x.y`或者`x[y]`也就比较好推断了。 但是如果`x`类型未知,是不是应该把`getattr`/`getitem`操作记录 HM 的方程里面, 等 unify x 时再去真正执行`getattr`/`getitem` ?

    3 . subtyping 好像是比较麻烦,如果在语法层面,把类继承禁用,是不是就没有 subtyping 的问题了呢?

    4. 我去学习一下 Typeclass ,Row Polymorphism
    secondwtq
        10
    secondwtq  
       104 天前   ❤️ 1
    @wcsjtu
    这些问题的答案其实严重依赖于你做的东西的具体需求和设计
    比如准确来说隐式转换也算 subtyping ,但是动态类型语言好像不存在这方面的问题,虽然如果你要性能非要用 unboxed native 的值表示那这个又必须要解决
    因为在运行之前动态类型语言其实是不存在一个确切的“类型”的。比如 def foo x = x + 1 ,x 是个 int ,那它此时就是个 int -> int ,x 是个 bool ,那它又是 bool -> int ,这个和传统 HM 那套是不一样的。单就这段程序来说,typechecker 得到的信息只有“若 x 的类型为 a ,存在函数 +: a -> int -> b”,然后你要做的就是想办法把这个信息记录下来,Typeclass 和 Row Polymorphism 之类的其实就是信息的表示方法。

    更 general 地说,基于 HM 可以延伸出一个更通用的框架,typechecker 会把 AST 转换成 constraint 的集合,然后再去求解这些 constraint 。HM 的 constraint 非常简单所以好解,但是如果把丰富下语义是可以解决更复杂的问题的,当然可能会比较慢,很多较新的静态类型语言都用了类似的思想,比如:
    https://github.com/apple/swift/blob/main/docs/TypeChecker.md
    https://kotlinlang.org/spec/type-inference.html
    https://rustc-dev-guide.rust-lang.org/type-inference.html

    不过这些都是静态类型语言的玩法,我暂时无法想像这种东西怎么在动态类型语言上 scale ... 其实动态类型语言用的好像都是不太一样的方法,我主要折腾静态类型语言所以不太熟悉。
    wcsjtu
        11
    wcsjtu  
    OP
       102 天前
    @secondwtq 非常感谢。 目前我们是打算用 Python 写业务逻辑,然后转 C++。 完全禁用了 Python 的动态特性,所以可以把 Python 看做静态语言。subtyping 问题, 能够用强制类型标注的手段解决么?

    大佬给的这三个链接信息量非常大, 我去好好阅读下。
    secondwtq
        12
    secondwtq  
       94 天前
    @wcsjtu 还是那句话,非常依赖于具体的细节
    比如“可以把 Python 看做静态语言”这一条,假设有 y = foo(x),在静态类型语言中,foo 一般有一个预定义的类型,比如需要一个 int 并返回一个 int ,这时如果 x 原本是个 float ,调用 foo 时会被 coerce 成 int ,但是在动态类型语言中,x 传进去之后依然是个 float ,并且可能在 foo 内一直以 float 的形式参与计算。自然就可以推出,在两种语言中实现并调用逻辑类似的 foo 函数,得到的 y 可能是不同的值。这两种情况的类型推导的处理方式也不一样。
    再比如“类型标注”这一条,如果可以做到所有的函数和函数参数、返回值以及 class 的成员都有类型标注,问题会 trivial 很多,因为这样就和普通的静态类型语言没啥区别了,甚至大多数情况下都不需要怎么“类型推导”,而只需要按程序顺序根据类型标注给出的信息 check 一下函数的形参和实参类型是否匹配,需要“推导”的主要是泛型参数和 lambda ,问题的规模一般都比较小。
    但是如果项目的目的是兼容一些已有的 Python 代码,那上面这两条都会有坑,所以我之前的看法一直都比较保守。
    关于   ·   帮助文档   ·   博客   ·   API   ·   FAQ   ·   我们的愿景   ·   广告投放   ·   实用小工具   ·   2589 人在线   最高记录 5497   ·     Select Language
    创意工作者们的社区
    World is powered by solitude
    VERSION: 3.9.8.5 · 33ms · UTC 04:07 · PVG 12:07 · LAX 20:07 · JFK 23:07
    Developed with CodeLauncher
    ♥ Do have faith in what you're doing.