是否可以通过映射函数和lambdas使Typed Racket推断类型

Question

在回答这个问题时，我发现您似乎经常需要为匿名函数的参数添加类型注释，这些函数用作映射函数的参数：map、foldl等等

这里有两个简单的例子(所有这些都假设#lang typed/racket，而我使用的是Racket8.0(

我希望这个工作：

(define (f (l : (Listof Number)))
: (Listof Number)
(map (λ (x)
(+ x 1))
l))

但事实并非如此：你需要告诉它，x的论点是Number:

(define (f (l : (Listof Number)))
: (Listof Number)
(map (λ ((x : Number))
(+ x 1))
l))

或者你可以使用for/list，现在你不需要注释：

(define (f (l : (Listof Number)))
: (Listof Number)
(for/list ([x (in-list l)])
(+ x 1)))

另一方面，这将起作用：

(define (g (l : (Listof Number)))
: Number
(foldl + 0 l))

但如果我用(有点傻，但我想要一个小例子(代替它

(define (g (l : (Listof Number)))
: Number
(foldl (λ (x y) (+ x y))  0 l))

它失败了，需要转换成

(define (g (l : (Listof Number)))
: Number
(foldl (λ ((x : Number) (y : Number)) (+ x y))  0 l))

正如我所看到的，只有当匿名函数作为参数传递时才会发生这种情况，因为这个(同样，愚蠢的(函数是可以的：

(define (gg (x : Number) (y : Number))
((λ (a b) (+ a b))
x y))

在最后一个函数中，您可以从GUI中看到，它已经成功地从x和y的类型推断出了a和b的类型。

我很容易对这里的一些事情感到困惑，然而，因为我甚至不能勉强胜任Typed Racket。

所以问题是：我是不是很困惑，这些匿名函数的参数类型真的不知道，或者这只是类型检查器(还(不够聪明，无法自行推断的情况？

Answer 1

我不知道你说的"不可知"；但这确实是Typed Racket的工作原理。如果应用多态函数，它不会使用参数的类型来推断其他参数的类型。但在最后一个例子中，它确实使用了参数的类型来推断参数的类型。