正确理解和使用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.现在,我想将此功能移动到键入的球拍中.这是我提出的类型声明:

(: 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不允许一次绑定多个虚线变量,因为不清楚如何实例化它们.这与您在同一功能中不能有多个休息参数的原因相同.

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