[ANN] "Type Coverage" - core.typed 0.2.3, lein-typed 0.3.0

[Ambrose Bonnaire-Sergeant]

Hi,

core.typed 0.2.3 is up, and comes with two new functions:

- statistics

- var-coverage

statistics returns a map of data on the results of type checking some namespaces. var-coverage is an example of how to leverage this data to write quick and easy aggregating functions.

This works well at the REPL, for example var-coverage accepts zero arguments for the current namespace.

clojure.core.typed.utils=> (t/var-coverage)

Start collecting clojure.core.typed.utils

Finished collecting clojure.core.typed.utils

Collected 1 namespaces in 347.052768 msecs

Checked 0 namespaces (approx. 0 lines) in 347.38633 msecs

Found 12 annotated vars out of 51 vars

23% var annotation coverage

nil

lein-typed 0.3.0 is also released, and supports a new coverage command. It requires core.typed 0.2.3 or later to use.

$ lein typed coverage

Initializing core.typed ...

"Elapsed time: 4505.279024 msecs"

core.typed initialized.

Start collecting typed-demo.core

Finished collecting typed-demo.core

Collected 1 namespaces in 4619.570363 msecs

Checked 0 namespaces (approx. 0 lines) in 4621.945525 msecs

Start collecting typed-demo.nil

Finished collecting typed-demo.nil

Collected 1 namespaces in 20.48361 msecs

Checked 0 namespaces (approx. 0 lines) in 20.645363 msecs

Found 2 annotated vars out of 2 vars

100% var annotation coverage

This is all part of Brandon Bloom's ideal vision of how types should be used in Clojure. Thanks for the great idea!

Enjoy!

Ambrose

[Brandon Bloom]

> lein-typed 0.3.0 is also released, and supports a new coverage command.

Awesome!

 

> This is all part of Brandon Bloom's ideal vision of how types should be used in Clojure. Thanks for the great idea!

Heh, you're welcome! Thanks for doing this & the shout out.

Just wanted to elaborate a little bit on the views I shared with Ambrose and why I pushed him to do this lein plugin, and then to add the coverage command. In short, I view types as just one more tool in the verification and correctness toolbox. They have lots of other uses, such as for aiding optimization in compilers, but they can (and should!) be part of a varied suite of tests for robust applications.

However, just as approaching 100% unit test coverage has diminishing returns, so does approaching 100% "type coverage". Type annotations can fit in right next to your unit and integration tests, outside of your src directory. Alternatively, you can include your type annotations inline, just like :pre and :post conditions, or validators. For modules that fit at the intersection of easily and precisely typed, core.typed can save you a lot of manual verification work!

As for the lein plugin, I think that low barriers to use will encourage more people to try core.typed as a verification tool. My dream is to be able to run a single command that infers all the types in my program, with separate annotations on the public interface from the private ones. Then I can then validate and check-in the public annotations and discard the private annotations. Whenever I change the public interface or experience cascading type inference failures in private code, I'd get a test error with lein. In this world, I can get 80% of the benefits of types with only 20% of the cost.

Cheers,

Brandon