瞭解和使用類型化球拍省略號正確

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，因爲他們在不同類型的使用。