Typed Racket: map list items while remembering individual types?

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.


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

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

1 Like

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