Typed Racket 的类型推断是如何工作的？

Posted 2023-02-21

【中文标题】Typed Racket 的类型推断是如何工作的？

【英文标题】：How does Typed Racket's type inference work?

【发布时间】：2012-10-14 19:55:15

【问题描述】：

Typed Racket 做了什么样的类型推断？我在 Racket 邮件列表中找到了以下 sn-p：

Typed Racket 类型系统包含许多功能 超出 Hindley/Milner 样式类型系统所支持的范围，等等 我们不能使用那个推理系统。目前，Typed Racket 使用 本地类型推断来推断程序中的许多类型，但是 我们想推断出更多——这是一个正在进行的领域 研究。

上面的简介使用术语“本地类型推断”，我也听说过很多使用“出现类型”，但我不确定这些术语是什么意思。

在我看来，Typed Racket 目前使用的类型推断系统过于薄弱。这是我的意思的一个例子。以下不输入检查：

(struct: pt ([x : Real] [y : Real]))

(define (midpoint p1 p2)
  (pt (/ (+ (pt-x p1) (pt-x p2)) 2)
      (/ (+ (pt-y p1) (pt-y p2)) 2)))

您必须用(: midpoint (pt pt -> pt)) 显式注释midpoint，否则会出现错误：Type Checker: Expected pt, but got Any in: p1。为什么类型检查器不能由此得出p1 和p2 的类型必须 是pt？这是 Racket 实现类型的方式的基本限制吗（即，由于 Racket 的一些更高级的类型特性，这种推理有时实际上是错误），还是可以实现的？未来？

【问题讨论】：

Sam Tobin-Hochstadt 的博士论文应该有血淋淋的细节：ccs.neu.edu/racket/pubs/dissertation-tobin-hochstadt.pdf

【参考方案1】：

默认情况下，假定未注释的***函数具有Any 的输入和输出类型。我提供了这个模糊的解释：由于 Racket 的类型系统非常灵活，它有时可以推断出你意想不到的类型，并允许某些程序在你可能希望它们发出类型错误时进行类型检查。

Tangent：如果适合您，您也可以使用 define: 表单。

(define: (midpoint [p1 : pt] [p2 : pt]) : pt
  ...)

【讨论】：

添加到这个答案：我会在一周中的任何一天接受“定义明确”而不是“聪明”。 “聪明”的问题在于，作为一名程序员，迟早你会在可检查和不可检查之间的边界的另一边结束，你必须弄清楚如何更改你的代码所以检查器可以验证它。在这种情况下，试图凭直觉判断要吸引哪种聪明才智可能非常困难。

所以听起来并没有真正的基本限制 - 相反，在类型良好的程序和不是的程序之间只有一个模糊的灰色区域（也许这个区域在 Typed Racket 中比其他类型系统更大，因为 Racket 系统非常灵活）。设计 Typed Racket 的推理的人只是尽可能地远离那个边界：只有少数定义明确的情况可以发生类型推理，其他一切都必须显式声明。这样，他们就避免陷入混乱。对吗？

@Ord 差不多。您可以阅读 Sam 的论文以了解详细信息。他甚至将其中的一部分专门用于这个问题：第 3.2 节。