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

[wcsjtu]

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

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

[pisc]

Type Inference 会用到很多 PL 知识，我觉得你应该先系统地补一下 PL 和 类型系统相关的知识（如果你没太多时间的话，可以简单看一下 http://lucacardelli.name/papers/typesystems.pdf ）？没有相关知识的话，感觉会比较吃力 ，你需要看透 Python 那些类型的实质是什么，比如 “struct”, tuple 和 product type 的关系，在 Python 这种语言上做类型系统本来就不是太容易，你可以看看某网红写的 https://github.com/yinwang0/pysonar2 （虽然可能不是你想要的 HM ）

[pisc]

可以直接说你的项目需求是什么，可能会比你问 HM 和 struct 之类的（因为这个路径可能是错的），别人更能帮助到你

[Austaras]

虽然不知道你说的 struct 是什么，但目测说的是 row poly ，那其实可以看看 elm 的实现，或者直接搜论文

[wcsjtu]

@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]

@Austaras 大佬能给个搜索关键字吗， 我不是 PL 背景出身……行业黑话看不懂啊

[Austaras]

row polymorphism 就是搜索关键字啊

[secondwtq]

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]

@Austaras 多谢大佬，我去学习下什么是 row polymorphism

[wcsjtu]

@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]

@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]

@secondwtq 非常感谢。 目前我们是打算用 Python 写业务逻辑，然后转 C++。 完全禁用了 Python 的动态特性，所以可以把 Python 看做静态语言。subtyping 问题， 能够用强制类型标注的手段解决么？

大佬给的这三个链接信息量非常大， 我去好好阅读下。

[secondwtq]

@wcsjtu 还是那句话，非常依赖于具体的细节
比如“可以把 Python 看做静态语言”这一条，假设有 y = foo(x)，在静态类型语言中，foo 一般有一个预定义的类型，比如需要一个 int 并返回一个 int ，这时如果 x 原本是个 float ，调用 foo 时会被 coerce 成 int ，但是在动态类型语言中，x 传进去之后依然是个 float ，并且可能在 foo 内一直以 float 的形式参与计算。自然就可以推出，在两种语言中实现并调用逻辑类似的 foo 函数，得到的 y 可能是不同的值。这两种情况的类型推导的处理方式也不一样。
再比如“类型标注”这一条，如果可以做到所有的函数和函数参数、返回值以及 class 的成员都有类型标注，问题会 trivial 很多，因为这样就和普通的静态类型语言没啥区别了，甚至大多数情况下都不需要怎么“类型推导”，而只需要按程序顺序根据类型标注给出的信息 check 一下函数的形参和实参类型是否匹配，需要“推导”的主要是泛型参数和 lambda ，问题的规模一般都比较小。
但是如果项目的目的是兼容一些已有的 Python 代码，那上面这两条都会有坑，所以我之前的看法一直都比较保守。