gpt4 book ai didi

types - 这两种类型注释有什么区别,为什么不同?

转载 作者:行者123 更新时间:2023-12-04 10:56:38 25 4
gpt4 key购买 nike

我试图从 Little Schemer 一书中为这个函数添加类型。

(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)))))

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

最佳答案

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

(: 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 的类型推断算法足够聪明,可以找出 ((rember-fc test?) a (cdr l)) 中的 forall 变量是什么。当 (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)))]))))

关于types - 这两种类型注释有什么区别,为什么不同?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/59132146/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com