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

Question

Typed Racket 做什么样的类型推断？我在 Racket 邮件列表中发现了以下片段:

The Typed Racket type system contains a number of features that go beyond what's supported in Hindley/Milner style type systems, and so we can't use that inference system. Currently, Typed Racket uses local type inference to infer many of the types in your program, but we'd like to infer more of them -- this is an ongoing area of research.

上面的介绍使用了术语“局部类型推断”，我也听说过很多次使用“发生类型”，但我不确定这些术语的含义。

在我看来，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 实现类型方式的基本限制吗(即，由于 Racket 的一些更高级的类型功能，这种推理有时实际上是错误的)，还是可能在 future 实现？

Answer 1

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

切线:您也可以使用 define:表格，如果那是适合你的。

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