Typed Racket: map list items while remembering individual types?

Questions & Answers
,
1

First, consider lists where all list items are the same time. I already know that this isn't possible the easy way due to nested polymorphic functions:

(map values '(5 6 7))
/!\ Type Checker: Polymorphic function `map' could not be applied to arguments

and I have to (inst values) to make it work:

(map (inst values Integer) '(5 6 7 8))
- : (Pairof Integer (Listof Integer))
'(5 6 7 8)

My real question is about mixed type lists. This is the shortest code that I could come up that maps the list while remembering the type of each list item. Notice how on this one I don't need to (inst values), instead, I have to type the input as (List a ...):

((lambda #:forall (a ...) ([xs : (List a ...)]) (map values xs)) '(5 a "s"))
- : (List Positive-Byte 'a String)
'(5 a "s")

Is there a way to do this that's more intuitive/requires fewer keystrokes? I've played around a fair bit and I can't find a shorter version. It would be okay if I could turn this into a macro, but I can't figure out how to do that either, because ... has special meaning in define-syntax-rule.

I don't want to use (inst values Any) because it would turn my list into (Listof Any), which forgets the list's length and the type of each item.

2

The feature you're using in the last example is exactly what's intended to express the pattern you want.

3

You can escape ... in templates by writing (... ...).

4

Thanks for the help! I ended up with this final code just like you described.

(define-syntax-rule (map-elements fn lst)
  (... ((lambda #:forall (a ...) ([xs : (List a ...)]) (map fn xs)) lst)))