Macro typing rules milestone: for+destructuring
Published on June 1, 2021 by Ambrose Bonnaire-Sergeant
Hi,
This week I made some exciting progress on a long standing challenge: a typing rule for `clojure.core/for`.
If you've used core.typed, you might remember certain macros cannot appear in typed code--for example you must use `clojure.core.typed/for` (with local annotations!) instead of `clojure.core/for`. This work on typing rules aims to lift this restriction by giving the type checker earlier access to form being checked, in particular before it has been fully expanded (and becomes an unintelligible mess, at least according to the checker).
A `for` typing rule has been an worthy goal since it has many parts:
- It introduces new bindings
- It supports destructuring, but does not directly destruct the right-hand side (if the right-hand side is (Seqable a), then it destructures a)
- It has an interesting return value (if the body returns a, the for returns (Seq a)), and thus propagating expected types is not immediate (if (Seq a) is expected, then a must be propagated as the expected type of the body).
Essentially, I feel `for` is a worthy road test for Typed Clojure's typing rules implementation. And over the weekend, I achieved a significant milestone: a `for` typing rule supporting destructuring.
As a direct comparison for end users, before you had to use:
(clojure.core.typed/for [a :- s/Int, (range 10)] a)
to write
(clojure.core/for [a (range 10)] a)
Now, the latter version just works, inferring (Seq Int).
Expected types propagate as expected:
(-> (clojure.core/for [a (range 10)] a) (ann-form (Seq Bool)))
now blames the `a` in the body for having type Int instead of Bool (before, the entire form was blamed, (Seq Int) instead of (Seq Bool)).
This is the second typing rules framework I've built for Typed Clojure, and I think it's flexible enough to (eventually) expose as a public API to teach the checker how to check your own macros.
Up next, I want to support the :let/:when/:while keywords of `for`, and also map destructuring (so far, I've only supported vector destructuring, but that's enough as a proof of concept).
Thanks all for your support!
Ambrose