[racket] Typed Racket has finally arrived!

Typed Racket has arrived: it is useful to write programs in it in which 
types outnumber code. From my dissertation project:

   (: make-rect-list-subtract-one
      (All (N1 F1 E1 V1 N2 F2 E2 V2)
           ((set-sig N1 F1 E1 V1)
            (set-sig N2 F2 E2 V2)
            -> ((Listof (Nonextremal-Pair-Rect N1 F1 N2 F2))
                (Nonextremal-Pair-Rect N1 F1 N2 F2)
                -> (Listof (Nonextremal-Pair-Rect N1 F1 N2 F2))))))
   (define (make-rect-list-subtract-one ops1 ops2)
     (define pair-rect-subtract (make-pair-rect-subtract ops1 ops2))
     (λ (As B)
       (append* (map (λ: ([A : (Nonextremal-Pair-Rect N1 F1 N2 F2)])
                       (pair-rect-subtract A B))
                     As))))


FWIW, this is my fault for using `case->' types in other spots to have 
TR prove extra stuff. Also, I'm manually doing generics. (Generic set 
operations come bundled in a `set-sig' with type parameters for 
*N*onextremal set, *F*ull (universal) set, *E*mpty set, and *V*alue.)

This is not a snarky complaint about lack of generics or too much typing 
(pun intended). Rather, I'm impressed that I can get TR to typecheck a 
"union of sets of pairs" function with this type:

   (case-> ((Pair-Set N1 F1 N2 F2) (Nonempty-Pair-Set N1 F1 N2 F2)
                                   -> (Nonempty-Pair-Set N1 F1 N2 F2))
           ((Nonempty-Pair-Set N1 F1 N2 F2) (Pair-Set N1 F1 N2 F2)
                                   -> (Nonempty-Pair-Set N1 F1 N2 F2))
           ((Pair-Set N1 F1 N2 F2) (Pair-Set N1 F1 N2 F2)
                                   -> (Pair-Set N1 F1 N2 F2)))

with only small changes to the function body. IOW, I can get it to prove 
that a union of a nonempty product set and a possibly empty product set 
is nonempty, mostly just by using more specific annotations.

I'm fine with large types that happen to be useful theorems. They've 
caught errors, made many dynamic checks unnecessary, and taught me 
things about the code I'm writing. Kudos to the TR team.

Also, it struck me as funny that I had written a useful function with 
more type than code. :D

Neil ⊥