这两种类型注释之间有什么区别，为什么它们不同?

Question

我试图从《小小策划者》一书中为这个函数添加类型。

(define rember-fc
(λ(test?)
(λ (a l)
(cond [(null? l) '()]
[(test? a (car l)) (cdr l)]
[else
(cons (car l)
((rember-fc test?) a (cdr l)))]))))

此类型会导致错误。

(: rember-fc  (∀ (a) (-> (-> Any Any Boolean)  (-> a (Listof a) (Listof a)))))

此类型有效。

(: rember-fc  (-> (-> Any Any Boolean)  (∀ (a) (-> a (Listof a) (Listof a)))))

我想知道为什么这两种类型会导致不同的结果，有什么区别？

Answer 1

该函数可以在类型签名的第一个版本下工作

(: rember-fc  (∀ (a) (-> (-> Any Any Boolean)  (-> a (Listof a) (Listof a)))))

如果在递归调用中使用该函数的位置添加注释，请将

((rember-fc test?) a (cdr l))

跟

(((inst rember-fc a) test?) a (cdr l))

其中inst类型注释允许它进行类型检查。

函数的这种用法有两个应用程序，一个内部应用程序和一个外部应用程序。首先对内部应用程序进行类型检查，而外部应用程序仅在具有内部应用程序的具体类型后进行类型检查。

Typed Racket的类型推断算法足够聪明，可以找出forall变量在((rember-fc test?) a (cdr l))中是什么，当(rember-fc test?)具有forall类型和a并(cdr l)提供信息时。如果 forall 位于中间，则内部应用程序不需要类型推断，并且外部应用程序类型推理成功，因为外部应用程序参数提供了信息。

但是，类型推断不够智能，无法确定rember-fc何时具有 forall 类型，并且test?不会在内部应用程序中提供信息。a和(cdr l)仅在稍后的外部应用程序中应用。当类型推断无法弄清楚时，它会在内部应用程序中猜测Any，并且稍后才会在外部应用程序中发现猜测是错误的。

所以两个工作版本是：

(: rember-fc  (∀ (a) (-> (-> Any Any Boolean)  (-> a (Listof a) (Listof a)))))
(define rember-fc
(λ (test?)
(λ (a l)
(cond [(null? l) '()]
[(test? a (car l)) (cdr l)]
[else
(cons (car l)
(((inst rember-fc a) test?) a (cdr l)))]))))

和：

(: rember-fc  (-> (-> Any Any Boolean)  (∀ (a) (-> a (Listof a) (Listof a)))))
(define rember-fc
(λ (test?)
(λ (a l)
(cond [(null? l) '()]
[(test? a (car l)) (cdr l)]
[else
(cons (car l)
((rember-fc test?) a (cdr l)))]))))