Applying to potentially empty lists in Typed Racket

Question

The following is no problem in untyped racket:

(apply hc-append
       (for/list ([colour '("red" "green" "blue")])
                 (colorize (filled-rectangle 10 10) colour)))

The result is a pict with three differetnly coloured squares.

But it's not possible in Typed Racket. First, for/list needs a type annotation:

  (apply hc-append
         (for/list : (Listof pict)
                   ([colour '("red" "green" "blue")])
           (colorize (filled-rectangle 10 10) colour)))

But then, the types of (curry apply hc-append) and the result of the (for/list …) form don't align:

; […] Type Checker: Bad arguments to function in `apply':
; Domains: pict pict *
;          Real pict pict *
; Arguments:  (Listof pict)

This error message looks puzzling, but it comes down to the fact that (Listof pict) may be empty, and hc-append's type signature requires pict pict *, i.e. at least one pict.

But this works in both typed and untyped Racket:

(apply hc-append (map (curry colorize (filled-rectangle 10 10))
                      '("red" "green" "blue")))

The type of the (map …) form is (Pairof pict (Listof pict)). Great! That's a non-empty list. But I can't use that in the for/list form as a type annotation, the type checker rejects it.

Even if I carefully pick apart the types:

(let ([potentially-empty-list
       (for/list : (Listof pict)
                 ([c '("red" "green" "blue")])
         (colorize (filled-rectangle 10 10) c))])
  (cond
    [(null? potentially-empty-list) (blank)]
    [else (apply hc-append #{(list (first potentially-empty-list)
                                   (rest potentially-empty-list))
                             : (Pairof pict (Listof pict))})]))

I end up with a very confusing message, essentially the same, but now it defies my original justification! Namely, that the list may be empty. The type clearly states that it may not be empty! Racket rejects it:

; […] Type Checker: Bad arguments to function in `apply':
; Domains: pict pict *
;          Real pict pict *
; Arguments:  (List pict (Listof pict))

Two things confuse me:

• Instead of my original (Pairof pict (Listof pict)), Racket turns the type into (List pict (Listof pict)). I think that's OK, because the two should be equivalent.
• But if they're equivalent then I would expect the (apply …) form to work, as in the (map …) case! There, too, we use (apply hc-append ls) where ls has type (Pairof pict (Listof pict)).

My intuiton is that at least the last example should work, but it does not, and I don't understand why.

Answer 1

Your following code is pretty close.

(let ([potentially-empty-list
       (for/list : (Listof pict)
                 ([c '("red" "green" "blue")])
         (colorize (filled-rectangle 10 10) c))])
  (cond
    [(null? potentially-empty-list) (blank)]
    [else (apply hc-append #{(list (first potentially-empty-list)
                                   (rest potentially-empty-list))
                             : (Pairof pict (Listof pict))})]))

However, there are two mistakes.

1. (list (first ....) (rest ...)) is a list of two elements, where the first element is a pict and the second element is a (Listof pict). I.e. it has type (List pict (Listof pict)). I think you instead want to use (cons (first ....) (rest ...)), which has type (Pairof pict (Listof pict) = (Listof pict) that guarantees it has at least one element.
2. You should use #{(cons ...) :: (Pairof ...)} instead. The #{x : t} notation is only valid in binding positions, particularly when x is a variable. The #{e :: t} notation however allows e to be an arbitrary expression, which is what you are doing here. Typed Racket does appear to be buggy in a sense that it doesn't report a misuse of #{x : t} when x is not a variable. I'll file a bug report.

Following program works:

#lang typed/racket

(require typed/pict)

(let ([potentially-empty-list
       (for/list : (Listof pict)
         ([c '("red" "green" "blue")])
         (colorize (filled-rectangle 10 10) c))])
  (cond
    [(null? potentially-empty-list) (blank)]
    [else (apply hc-append #{(cons (first potentially-empty-list)
                                   (rest potentially-empty-list))
                             :: (Pairof pict (Listof pict))})]))