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实现类型的方式的一个基本限制(也就是说,由于某些Racket更高级的类型特性,这种推理方式实际上有时是错误的),或者这是否有可能在未来实现？

Answer 1

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

Tangent:define:如果适合您,您也可以使用表格.

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