FWIW I've been pushing Typed Clojure in interesting directions that can be directly applied back to Typed Racket. The implementations are so similar that there is good potential for cross pollination.
Fair enough, it does sound like an interesting research project, I'm just not sure what will come of it. Can you make any speculations about what those directions might be? Or is it too early?
Edit: global type inference? I thought that was infeasible for TR and Clojure at the moment?
The type system's interaction with Java's type system is interesting, which is something I've fleshed out.
I have heterogeneous maps as well as heterogeneous vectors, and support complex operations like merge. Unsure if relevant to Racket.
There are lots of other ideas which I need to implement to type check Clojure, but aren't necessarily crucial to type checking Racket, but would be nice to have.
One of the TR maintainers (samth?) told me on IRC a while ago that it is very infeasible to do global type inference (top level) for TR. So I'm not sure how much you could get done in so short a time.
Yep that's correct. I want a tool that infers a rough approximation of top-levels to accelerate the process of porting untyped code to be typed. The programmer would inspect the annotations manually and fix any inaccurate ones, and then run the type checker.
I believe it has to do with features like subtyping and method overloading which cause havok for global type inference. Found a paper here: http://ropas.snu.ac.kr/lib/dock/HoMi1995.ps