An answer to CircleCI's "Why we’re no longer using Core.typed"
CircleCI has recently published a very useful post "Why we’re no longer using Core.typed" that raises some important concerns w.r.t. Typed Clojure that in their particular case led to the cost overweighting the benefits. CircleCI has a long and positive relation to Ambrose Bonnaire-Sergeant, the main author of core.typed, that has addressed their concerns in his recent Strange Loop talk "Typed Clojure: From Optional to Gradual Typing" (gradual typing is also explained in his 6/2015 blog post "Gradual typing for Clojure"). For the sake of searchability and those of us who prefer text to video, I would like to summarise the main points from the response (spiced with some thoughts of my own).
Disclaimer: All the useful information comes from Ambrose. All the errors and misinterpretations, if any, are mine.
(It should be noted that CircleCI has quite a large codebase with ~ 90 typed namespaces.)
Summary: The situation is already better and will be much better when gradual typing is fully finished.
#1 Slow checking - this is already solved by the Typed REPL and the caching built into require / load.
Ambrose Bonnaire-Sergeant (ABS): But the Typed REPL is still work in progress, "In particular, it doesn't play nicely with many tools that use the current namespace to evaluate tools-specific things (eg. autocompletions). [...] it's undocumented and unproven" though the require/load caching might be split out and used separately as it doesn't suffer from these problems.
#2 Mixing of typed and untyped code and thus lack of compile-time guarantees - this will be solved by gradual typing when finished by adding runtime checks to these types (and adding runtime checks to ensure that untyped code cannot pass illegal values to typed code)
#3 Expressions that are impossible / hard to type - I don't think this has been addressed in the talk, though I have seen in the Google Group that the community continually thinks about ways to be able to type more Clojure idioms. My thoughts: There should be a first-class support for these, i.e. a well known, well supported and easy to use way to work around these. Something like the solution for external untyped code where we provide our own type signature and mark it with ":no-check". (Though I obviously have no idea what this solution for the particular problem of type uncheckable expressions would be.) Also, it should not be impossible to modify the error reporting to clearly distinguish errors caused by core.typed's limitations and those by defects in the code being checked.
ABS: "The most significant work on this front (ie. supporting more idioms at compile-time) has been incremental since 2013. Overhauls are needed for the challenges CircleCI use as examples."
#4 Cost of maintaining type signatures for 3rd party libraries - this will be still costly but much more valuable and reliable as these types will be turned into runtime guarantees. My thoughts: This is no different from using Prismatic Schema, there you too need to check that external code conforms to your contracts.
ABS: One interesting idea is to convert existing Schema annotations to core.typed for libs that have them.
#5 The difficulty of finding out the right type signatures of more complex functions - this hasn't been addressed. My thoughts: Making it easier to derive type signature is certainly an interesting are for exploration though likely outside of the main focus now. It would be great to run a function with few examples of its usage through some magical box and get back a type signature for it :-)
ABS: "I'm personally mostly interested in using compile-time data to infer types at the moment, which would again require some overhauls if at all possible. Your suggestion has been successfully used in practice though, see DRuby. I would like to know if this approach works on typical Clojure code. IME types in many Clojure programs aren't especially polymorphic or higher-order when crossing function boundaries, functions often take a map or some other simple value, so there's probably something worth investigating."
Core.typed is relevant and useful in many cases. With the progress towards Gradual Typing it will become even much more powerful and useful on mixed typed-untyped code based.
Disclaimer: All the useful information comes from Ambrose. All the errors and misinterpretations, if any, are mine.
The concerns
(It should be noted that CircleCI has quite a large codebase with ~ 90 typed namespaces.)
- Slow checking - If you work on multiple files, you need to re-scan them all which takes very long time on a large project
- Mixing of typed and untyped code and thus the use of types with :no-check leads to weakened guarantees; both inside one's own codebase and when interacting with untyped libraries (see #4).
- Some expressions cannot by typed (get-in, ...) and it is difficult to distinguish whether an error is caused by core.typed's limitations or an actual defect in the code being checked
- It's costly to maintain type for untyped 3rd-party libraries
- It is difficult to find out the right type signature for some expressions
The solutions
Summary: The situation is already better and will be much better when gradual typing is fully finished.
#1 Slow checking - this is already solved by the Typed REPL and the caching built into require / load.
Ambrose Bonnaire-Sergeant (ABS): But the Typed REPL is still work in progress, "In particular, it doesn't play nicely with many tools that use the current namespace to evaluate tools-specific things (eg. autocompletions). [...] it's undocumented and unproven" though the require/load caching might be split out and used separately as it doesn't suffer from these problems.
#2 Mixing of typed and untyped code and thus lack of compile-time guarantees - this will be solved by gradual typing when finished by adding runtime checks to these types (and adding runtime checks to ensure that untyped code cannot pass illegal values to typed code)
#3 Expressions that are impossible / hard to type - I don't think this has been addressed in the talk, though I have seen in the Google Group that the community continually thinks about ways to be able to type more Clojure idioms. My thoughts: There should be a first-class support for these, i.e. a well known, well supported and easy to use way to work around these. Something like the solution for external untyped code where we provide our own type signature and mark it with ":no-check". (Though I obviously have no idea what this solution for the particular problem of type uncheckable expressions would be.) Also, it should not be impossible to modify the error reporting to clearly distinguish errors caused by core.typed's limitations and those by defects in the code being checked.
ABS: "The most significant work on this front (ie. supporting more idioms at compile-time) has been incremental since 2013. Overhauls are needed for the challenges CircleCI use as examples."
#4 Cost of maintaining type signatures for 3rd party libraries - this will be still costly but much more valuable and reliable as these types will be turned into runtime guarantees. My thoughts: This is no different from using Prismatic Schema, there you too need to check that external code conforms to your contracts.
ABS: One interesting idea is to convert existing Schema annotations to core.typed for libs that have them.
#5 The difficulty of finding out the right type signatures of more complex functions - this hasn't been addressed. My thoughts: Making it easier to derive type signature is certainly an interesting are for exploration though likely outside of the main focus now. It would be great to run a function with few examples of its usage through some magical box and get back a type signature for it :-)
ABS: "I'm personally mostly interested in using compile-time data to infer types at the moment, which would again require some overhauls if at all possible. Your suggestion has been successfully used in practice though, see DRuby. I would like to know if this approach works on typical Clojure code. IME types in many Clojure programs aren't especially polymorphic or higher-order when crossing function boundaries, functions often take a map or some other simple value, so there's probably something worth investigating."
Conclusion
Core.typed is relevant and useful in many cases. With the progress towards Gradual Typing it will become even much more powerful and useful on mixed typed-untyped code based.
Useful additional resources
- core.typed e-mail group - f.ex. "Future directions for core.typed" from 7/2015
- Wiki: Limitations of core.typed
- core.typed Jira
Key slides from the talk
