First Impressions with Typed Racket
I had a blast attending RacketCon 2018. Besides some great talks (check out Nadeem Abdul Hamid's talk on Sinbad), I also learned about a lot of neat stuff going on in the Racket world (for example, I discovered both the macro and feature profilers).
One particularly enjoyable bit was attempting to port a part of Herbie to Typed Racket, under Sam Tobin-Hochstadt's supervision. Typed Racket is Racket plus sound gradual typing. This means that all functions get types, and those types are checked every time the functions are called. It makes it easier to avoid type errors, and unlike the Racket contracts system it often comes with no runtime cost (and in fact some possible slight speedups).
After porting Herbie's regime inference subsystem, my initial thoughts are that Typed Racket is impressively complete—it is much more than just a research prototype—but that it still has plenty of rough edges. I am extremely impressed that Typed Racket could be applied to a single file in a larger system, and that the transition could happen in an afternoon even in a fairly mature project. I also did not pick the easiest file to transition first, so I ended up having to write signatures for many other methods in Herbie, just to be able to use them.
Despite that, I got the job done, and though I had some help from Sam ultimately the process was not super-mysterious, just a bit tedious.1 [1 I also found a few different Typed Racket bugs, which Sam filed and fixed.] I did want to list some pain points that came up multiple times. Three come to mind.
For loops
First, for loops were a consistent challenge. Racket's variety of for
macros are great: for/list, but also for/and, for/first, and a few
others. Of course, assigning types to for loops is not in itself a
huge challenge. However, Typed Racket sees code post-macro-expansion,
so instead of seeing a for loop it sees some crazy recursive function.
This makes assigning types quite hard, and I found that I needed extra
annotations on a lot of my for loops, even if it didn't look like
anything interesting was going on in the loop. This was frustrating.
For things outside for/list, it was even worse. For example, I used a
for/or loop in one spot to return the first element satisfying some
property. Thus, I needed to return an element of type (U Boolean X).
However, internally, for/or expands to a mutable variable initialized
to #t, which is inferred to have type Boolean, so it becomes illegal
to store an X into it. I ended up rewriting a few for loops into named
let expressions, which were easier to type and type check, but harder
to read.
Generics
In Herbie, we are fairly heavy users of the dict and set generics. The
dictionary methods are really convenient to apply to association
lists,2 [2 They're certainly better than assq and friends!] and the
set methods don't have convenient list analogs. But Typed Racket has
minimal support for generics! This means that the dict methods don't
apply to anything, and the set methods only apply to hash-sets, not to
lists.
Typed Racket supports multiple types for functions, so it's possible
that this can be "patched up": add types to the dict and set methods
for at least the common instances of those generics. (Sam has now done
something like that.) Proper support for generics is likely harder,
but also probably rarely used.3 [3 Sam tells me he has an MS student
working on it.] The only generics we instantiate in Herbie are for
equality and for printing; those don't need type checking since
they're never directly called.
Equality
When Typed Racket interacts with non-typed code, it uses contracts to ensure that only well-typed inputs are passed into the typed part. This is mostly fine; however, sometimes those contracts change the behavior of code. In Herbie's case, all of the problems came from equality.
When you use parametric types in Typed Racket—like when, say, you
assign set-union the type (All (a) (-> (Set a) (Set a) (Set a))) Typed
Racket will try to prevent the internals of that code from looking
into the values of type a, since they need to be treated like a
black-box value to achieve parametricity. Typed Racket does this by
wrapping them in an opaque box that refuses to reveal its contents. So
far so good. However, these opaque boxes are now no longer equal?; if
you put the same thing in two different boxes, the result is two
different things. This makes functions like set-intersect misbehave
(returning the empty list), and those bugs are tricky to track down,
since they type check and then occur at runtime.
It seems to me like this problem is bad enough that it's worth giving
up parametricity: equal? should be able to peer through these opaque
boxes. But another approach would be doing something like tracking
type classes, and making sure that if you call a function that uses
equal?, that your function also needs to be annotated to track that
capability. Either approach is fine, but right now, Typed Racket can
actually add bugs to your code instead of removing them.
Conclusion
As I mentioned, Typed Racket is impressive, and dropping it into your
project is pretty doable, even if you have an old and mature codebase.
The require/typed macro makes it possible to migrate your application
to types one bit at a time, and once the types are there you will
forever have some extra assurance that type errors will not occur.
That said, there are still some pain points in Typed Racket today—pain
points I am sure Sam and his colleagues are working hard on fixing.
As for the part of Herbie I ported… we're still thinking about whether to keep it. It's an error-prone part of the code, and we've even had some bad type errors here in the past. But I doubt I have the time to migrate the rest of Herbie, nor am I sure I want to continue living in a typed world, at least while the restrictions I mentioned above are still there. For now, I think I'll be keeping it in a branch and thinking about transitioning other subsystems when I look at them.