4

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

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

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

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

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

  • lift取 ( B0, B1, ...Bn的函数C) 并产生：
  • 许多函数的函数（Aito Bi，i从 0 to 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）。我也不是很明白。

4

1 回答 1

5

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

至于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因为它们用于不同的类型。

于 2012-12-13T20:34:15.370 回答