Understanding and using Typed Racket ellipsis properly

Question

I want to define a function like this:

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

This basically "lifts" a function fn so that instead of accepting its normal arguments, it accepts functions and produces a new function. So, for example,

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

This works in plain Racket. Now, I want to move this function into typed racket. Here is the type declaration I came up with:

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

Here is what I think the definition says: For all types A0, A1, .. An and B0, B1, ... Bn, and C:

• lift takes (a function of B0, B1, ... Bn to C) and produces:
• a function of many functions (Ai to Bi, i from 0 to n) which in turn produces:
• a function of Ai, i from 0 to n, which in turn produces:
• a C

This doesn't work: in the last line (A ... B -> C) I get Type Checker: Type variable A must be used with ... in: A.

This isn't the first problem with ellipsis I've had while using Typed Racket, and I think it's really a case of fundamental misunderstanding of what the ellipsis is meant to do.

As a side note, if I try to collapse the All clauses to a single one like this:

(All (A ... B ... C) blah blah blah)

then in the second line ((B ... B - C) -> I get the following error: Type Checker: Used a type variable (B) not bound with ... as a bound on a ... in: B (referring to the second B on that line). I don't really understand that either.

Answer 1

To answer your last question first, the type syntax of All doesn't permit binding multiple dotted variables at once, because it wouldn't be clear how to instantiate them. This is the same reason you can't have multiple rest parameters in the same function.

As to lift, I think the type you want is:

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

And then the function goes through with one annotation:

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

Using this function requires some explicit annotation because of the nested foralls; here are your test cases:

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

Note that I had to create a separate binding for add2 because they're used at different types.