Hacker News new | ask | show | jobs
by anaphor 4654 days ago
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?
2 comments
ambrosebs 4654 days ago
Speaking speculatively, improving type inference is a great place for collaboration.

Concretely, I've extended several minor ideas.

Typed Clojure uses occurrence typing in sequential forms, as well as conditionals: http://frenchy64.github.io/2013/09/08/simple-reasoning-asser...

We can type check (filter identity coll) a little more accurately (which is actually quite hard to do): https://github.com/clojure/core.typed/blob/master/src/main/c...

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.

link
ambrosebs 4654 days ago
Also I'm not aware of a tool to "guess" top level annotations for Typed Racket. This is an area I want to explore further, soon.
link
anaphor 4654 days ago
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.
link
ambrosebs 4654 days ago
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.
link
moomin 4654 days ago
I'm far from an expert on this, but F# has no requirement for all forms to be explicitly typed, so I'm a bit puzzled as to why this is hard.
link
ambrosebs 4654 days ago
Typed Clojure's type system is too rich to avoid top-level annotations. It's a similar situation to Scala.
link
anaphor 4653 days ago
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
link