了解和使用类型化球拍省略号正确

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

这在普通球拍中起作用。现在，我想把这个功能转换为打字球拍。这里是我想出了类型声明：

(: 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），其又产生：
• 的Aii的函数，从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的类型语法不允许一次绑定多个虚线变量，因为不清楚如何实例化它们。这与你在同一个函数中不能有多个休息参数的原因是一样的。

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