Typed Racket的类型推断工作原理是什么？

Question

Typed Racket使用哪种类型推断？我在Racket邮件列表中找到了以下代码片段：

“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并使用(: midpoint (pt pt -> pt))，否则你会得到错误：Type Checker: Expected pt, but got Any in: p1。为什么类型检查器不能从中推断出p1和p2的类型必须是pt？这是Racket实现类型的基本限制（即由于一些更高级的类型特性，这种推理方式有时实际上是错误的），还是未来可能实现的内容？

- Ord

---

Sam Tobin-Hochstadt的博士论文应该有详细内容：http://www.ccs.neu.edu/racket/pubs/dissertation-tobin-hochstadt.pdf - dyoo

Answer 1

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

副题：如果适合您，还可以使用define:表单。

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

- Dan Burton

---

补充一下这个答案：我每天都会选择“定义明确”而不是“聪明”。 “聪明”的问题在于，作为程序员，迟早你会发现自己处于可检查和不可检查之间的边界上，你必须想办法改变你的代码，以便检查器可以验证它。在这种情况下，试图直觉地诉诸于哪种聪明才智可能非常困难。 - John Clements

听起来似乎并没有真正的基本限制 - 相反，只是在良好类型化的程序和不良类型化的程序之间存在这种模糊的灰色地带（也许在Typed Racket中这个区域比其他类型系统更大，因为Racket系统非常灵活）。设计Typed Racket推理的人只是尽可能远离那个边界：只有少数几种明确定义的情况下才能进行类型推断，其他所有情况都必须明确声明。这样，他们避免了陷入混乱的局面。这样说对吗？ - Ord

@Ord 这就对了。你可以阅读Sam的论文来了解细节。他甚至专门在第3.2节中探讨了这个问题。 - Dan Burton