types - 正确理解和使用 Typed Racket 省略号

Question

我想定义一个这样的函数:

(define (((lift fn) . gs) . args)
  (apply fn (map (lambda (g) (apply g args)) gs)))

这基本上“提升”了一个功能 fn所以它不是接受它的普通参数，而是接受函数并产生一个新函数。所以，例如，

 (define add (lift +))
 (define sum-of-sin-and-cos (add sin cos))
 (sum-of-sin-and-cos 5) ; is equivalent to (+ (sin 5) (cos 5))

 (define sum-of-multiplication-and-division (add * /))
 (sum-of-multiplication-and-division 1 2 3 4 5) ; is equivalent to (+ (* 1 2 3 4 5) (/ 1 2 3 4 5))

这适用于普通 Racket 。现在，我想将此功能移动到打字 Racket 中。这是我想出的类型声明:

(: lift (All (A ... ) (All (B ...) (All (C)
             ((B ... B -> C) ->
                     ((A -> B) ... B ->
                               (A ... B -> C)))))))

这是我认为定义所说的:对于所有类型 A0 , A1 , .. An和 B0 , B1 , ... Bn , 和 C :

lift取(B0、B1、...Bn 到 C 的函数)并产生:

许多函数的函数( Ai 到 Bi ，i 从 0 到 n )依次产生:

Ai 的函数, i从 0 到 n ，进而产生:

一个 C

这不起作用:在最后一行 (A ... B -> C)我得到 Type Checker: Type variable A must be used with ... in: A .

这不是我在使用 Typed Racket 时遇到的第一个省略号问题，而且我认为这确实是对省略号的含义的根本误解。

作为旁注，如果我尝试折叠 All像这样的单个子句:
(All (A ... B ... C) blah blah blah)
然后在第二行 ((B ... B - C) ->我收到以下错误: Type Checker: Used a type variable (B) not bound with ... as a bound on a ... in: B (指该行的第二个 B)。我也不是很明白。

Answer 1

首先回答你的最后一个问题，All 的类型语法不允许一次绑定(bind)多个虚线变量，因为不清楚如何实例化它们。这与您不能在同一函数中具有多个剩余参数的原因相同。

至于lift ，我认为你想要的类型是:

(: lift (All (C A ...)
             (All (B ...)
                  ((B ... B -> C)
                   ->
                   ((A ... A -> B) ... B 
                    ->
                    (A ... A -> C))))))

然后该函数通过一个注释进行:

(define (((lift fn) . gs) . args)
  (apply fn (map
             (λ: ([g : (A ... A -> B)])
               (apply g args))
             gs)))

由于嵌套的foralls，使用此函数需要一些显式注释；这是您的测试用例:

(define add ((inst (inst lift Number Number) Number Number) +))
(define add2 ((inst (inst lift Number Number Number Number Number Number)
                    Number Number)
              +))
(define sum-of-sin-and-cos (add sin cos))
(sum-of-sin-and-cos 5) ; is equivalent to (+ (sin 5) (cos 5))
(define sum-of-multiplication-and-division (add2 * /))    
(sum-of-multiplication-and-division 1 2 3 4 5)

请注意，我必须为 add2 创建单独的绑定(bind)。因为它们用于不同的类型。