UPDATE 4: Blog post: Inferring function types
UPDATE 3: Blog post: Basics of Automatic Annotations
UPDATE 2: A runnable demo is now available on Github! Try it out!
UPDATE 1: Blog post Introducing Automatic Annotations!
My name is Ambrose Bonnaire-Sergeant and I am implementing automatic type annotations for Typed Clojure.
Here's the main idea: we can use tests to generate types. We already write tests to specify our functions, what if we could also use them to generate type annotations?
To type check untyped code, you must write type annotations. Unfortunately, they are very annoying to write! When CircleCI abandoned Typed Clojure, they cited the annotation burden as a top reason for doing so. Even though they loved the key ideas underlying the type system, annotations were just too much work.
![]()
This is why automatic annotations are so badly needed: with this tool, you can get the benefits of a type system, without the tedium of writing annotations manually.
How to use it
To generate annotations for your namespace, simply:
- add core.typed metadata to your namespace,
-
run your unit tests for the namespace,
- run clojure.core.typed/runtime-infer in the current namespace.
Voila! Here's what our prototype produces.
The Benefits
Annotations help us do more than just type check untyped code.
Other benefits include:
documenting code: We can answer questions like "Given the current inputs/outputs, what kind of function have we written?". We can ask questions like this at any time in development.
-
runtime checking: Annotations can also be enforced at runtime, using infrastructure developed for Gradual Typing, my previous campaign.
- generative tests: We could even use the automatic annotation infrastructure to generate clojure.spec generative tests!
The Plan
I have already developed a prototype that generates type annotations for a subset of Clojure programs.
We plan to release this prototype in a future core.typed release (preview branch). The prototype infers function types, recursive map types, immutable collections, mutable atoms, and other base types.
From here, we plan to test our prototype against a suite of popular Clojure libraries. We will compile, evaluate, and release these results, then iterate on our prototype.
There are several dimensions to improve the generated types, including:
-
correctly chosen recursive types: generated nested types are squashed into recursive types based on a configurable algorithm. The correct choice will be based on real-world trials.
-
well named aliases: type aliases are used to share commonly occurring types between functions. Choosing good names for these aliases helps readability.
-
suitability for type checking: type annotations are used as fuel for type checking Clojure code. If a generated annotation successfully checks the definition and most usages of a function, then it's probably a good annotation.
We are aiming to submit an ICFP paper (due ~February).
The Feedback
I will keep everyone posted on our progress via my Twitter and my blog. Major releases will be announced on the core.typed mailing list. Our paper drafts will also be made publicly available. Why I need your help
If you are excited about this project and want to help it succeed, funding this campaign is the best way to support me. This campaign will help me to:
-
attend industrial conferences like Strangeloop, Clojure/conj, Clojure West, and Curry On,
- connect with the Clojure community via local meetups, and
- sustain my PhD program by staying out of debt.
Funds donated from the programming community have been vital in my progress with Typed Clojure.
Your support is greatly appreciated, and I hope you're just as excited as I am about the future of Typed Clojure!
Thanks for your contributions!
