How to Use Bounded and Rest Types Together?

23 views Asked by At

Supose a type similar to Haskell State Byte a, and a function that accepts many F's of the same input types, ignores each's non-byte output, and sums their byte outputs.

(define-type (F b a ...) (-> a ... a (Values b (Listof Byte))))

(: f+ (∀ (a ...) (->* () #:rest (F Any a ... a) (F Void a ; error on this a
                                                   ... a))))
(define (f+ . fs)
  (λ [args : a ... a]
    (values (void)
            (foldl (λ ([f : (F Any a ... a)] [acc : Byte])
                     (let-values ([(_ b) (apply f args)]) (+ acc b)))
                   0
                   fs))))

but i get the error that "type variable must be used with ...," regarding a.

thinking that there was a problem with ->* (btw i tried versions with -> and got the same error) i tried letting racket infer the type, but that just moved the location of the same error:

(define (f+ . fs)
  (λ #:forall (a ...) [args : a ... a]
    (values (void)
            (foldl (λ ([f : (F Any a ; error's here now!
                                ... a)]
                       [acc : Byte])
                     (let-values ([(_ b) (apply f args)]) (+ acc b)))
                   0
                   fs))))

obviously a is being used with ..., but i can't figure-out what i'm missing.

0

There are 0 answers