racket - 为什么 `filter` 使用高阶出现类型？

Question

在 Racket 的主页上，他们展示了这个例子:

#lang typed/racket
;; Using higher-order occurrence typing
(define-type SrN (U String Number))
(: tog ((Listof SrN) -> String))
(define (tog l)
  (apply string-append (filter string? l)))
(tog (list 5 "hello " 1/2 "world" (sqrt -1)))

我知道对于出现类型，像 (if (string? v) ...) 这样的表达式将标记v具有类型 String在真正的分支。这是因为 string? 的类型上面有一个过滤器:

> string?
- : (Any -> Boolean : String)
#<procedure:string?>

因此，对于“高阶出现类型”与 filter 一起工作函数，我希望类型为 filter说谓词类型的过滤器传播到结果类型。但是当我检查 filter 的类型时在 REPL 中，这不会显示:

> filter
- : (All (a b) (case-> ((a -> Any) (Listof a) -> (Listof b)) ((a -> Any) (Listof a) -> (Listof a))))
#<procedure:filter>

但这不可能是filter的真实类型，因为对 b 没有限制!我期待像

(All (a b) (a -> Any : b) (Listof a) -> (Listof b))

tldr:为什么 filter似乎在其返回类型中有一个不受约束的类型变量？

编辑:我正在使用 Racket v6.0

Answer 1

在Typed Racket Reference据说:

In some cases, asymmetric type information is useful in filters. For example, the filter function’s first argument is specified with only a positive filter. Example:

> filter
- : (All (a b)
      (case->
       (-> (-> a Any : #:+ b) (Listof a) (Listof b))
       (-> (-> a Any) (Listof a) (Listof a))))
#<procedure:filter>

The use of #:+ indicates that when the function applied to a variable evaluates to a true value, the given type can be assumed for the variable. However, the type-checker gains no information in branches in which the result is #f.

换句话说，如果您有以下示例:

> (filter string? '(symbol 1 2 3 "string"))
- : (Listof String)
'("string")

只有当string? 在其上返回 true。只有在这种情况下，才会传播过滤器谓词的类型。