实现类型推断

Posted 2023-02-19

技术标签:

【中文标题】实现类型推断【英文标题】：implementing type inference 【发布时间】：2010-09-29 18:07:01 【问题描述】：

我在这里看到了一些关于静态与动态类型的有趣讨论。由于编译类型检查、更好的文档化代码等原因，我通常更喜欢静态类型。但是，我同意如果按照 Java 的方式完成，它们确实会使代码变得混乱。

所以我即将开始构建我自己的函数式风格语言，类型推断是我想要实现的事情之一。我明白这是一个很大的课题，我并不想创造一些以前没有做过的东西，只是基本的推理......

关于阅读内容的任何指示对我有帮助吗？最好是更实用/实用的东西，而不是更理论的类别理论/类型理论文本。如果那里有实现讨论文本，带有数据结构/算法，那就太好了。

【问题讨论】：

正是我正在寻找的问题，有一些很好的答案！ 【参考方案1】：

我发现以下资源有助于理解类型推断，按难度递增顺序排列：

编程语言：应用和解释

Interpreting types as abstract values

编程语言基础

类型和编程语言

编程语言中的设计概念

但是，由于最好的学习方式是做，我强烈建议通过编程语言课程的家庭作业来实现玩具函数语言的类型推断。

我推荐这两个易于理解的 ML 作业，你们都可以在不到一天的时间内完成：

PCF Interpreter (a solution) 热身。 PCF Type Inference (a solution) 为 Hindley-Milner 类型推断实现算法 W。

These assignments 来自更高级的课程：

Implementing MiniML

Polymorphic, Existential, Recursive Types (PDF)

Bi-Directional Typechecking (PDF)

Subtyping and Objects (PDF)

【讨论】：

只是我，还是 PLAI 描述在很大程度上不正确/不完整？ The lecture 增加了一点，但似乎仍然不足以让它工作。 2012版PLAI书里的算法我也拿不到。约束列表没有替换。相反，我在 PLAI 书的 2003-7 版本中实现了类型推断算法，它似乎工作得更好，并且也可以很好地扩展到 let-polymorphism。 recon 和 fullrecon 链接好像坏了。 gziped 版本仍然可用：recon.tar.gz、fullrecon.tar.gz。【参考方案2】：

不幸的是，关于这个主题的许多文献都非常密集。我也站在你的立场上。我从 Programming Languages: Applications and Interpretation 中获得了对该主题的第一次介绍

http://www.plai.org/

我将尝试总结抽象的想法，然后是我没有立即发现的细节。首先，类型推断可以被认为是生成然后解决约束。要生成约束，您需要遍历语法树并在每个节点上生成一个或多个约束。例如，如果节点是+ 运算符，则操作数和结果都必须是数字。应用函数的节点与函数结果的类型相同，以此类推。

对于没有let的语言，可以盲目的通过替换来解决上面的约束。例如：

(if (= 1 2) 
    1 
    2)

在这里，我们可以说if语句的条件必须是布尔值，并且if语句的类型与其then和else子句的类型相同。由于我们知道1 和2 是数字，通过替换，我们知道if 语句是一个数字。

事情变得令人讨厌的地方，我有一段时间无法理解的是处理 let：

(let ((id (lambda (x) x)))
    (id id))

在这里，我们将id 绑定到一个函数，该函数返回您传入的任何内容，也称为身份函数。问题是函数参数x 的类型在id 的每次用法上都不同。第二个id 是a -> a 类型的函数，其中a 可以是任何东西。第一个是(a -> a) -> (a -> a) 类型。这称为 let 多态性。关键是按特定顺序求解约束：首先求解id 定义的约束。这将是a -> a。然后可以将id 类型的新的、单独的副本替换到使用id 的每个位置的约束中，例如a2 -> a2 和a3 -> a3。