Pavel Panchekha

By

Share under CC-BY-SA.

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.

Footnotes:

1

I also found a few different Typed Racket bugs, which Sam filed and fixed.

2

They're certainly better than assq and friends!

3

Sam tells me he has an MS student working on it.