14

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。为什么类型检查器不能由此得出p1and p2 must be的类型pt？这是 Racket 实现类型的方式的基本限制（即，由于 Racket 的一些更高级的类型特性，这种推理有时实际上是错误的），还是将来可能会实现？

4

1 回答 1

6

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

切线：define:如果适合您，您也可以使用表格。

(define: (midpoint [p1 : pt] [p2 : pt]) : pt
  ...)
于 2012-10-24T20:07:52.797 回答