[ANN] core.typed 0.2.0 - Production Ready

[Ambrose Bonnaire-Sergeant]

Hi,

After 10 months and 26 0.1.x releases of transitioning core.typed from an ambitious student project, I am finally comfortable recommending core.typed for production use.

Production Ready

My interpretation of "production ready" in this context is:

- core.typed can find bugs in real code

- core.typed will not slow down your existing code by loading

  a large library at production. (core.typed does introduce an extra "identity-like"

  function call at type annotations, I assume this is a candidate for optimisation via

  HotSpot)

- A basic tutorial, API docs and example project exist

- core.typed is currently used in production with success (at CircleCI for several months)

- The core type checking API is mostly stable, with only very

  minor removals/breaking changes in the last few months.

There are several outstanding issues, but I am satisfied that core.typed can bring real utility to real programs today and with no production-time drawbacks, thus this release.

How to get started

Leiningen dep:

[org.clojure/core.typed "0.2.0"]

...
; for very recent releases
:repositories {"sonatype-oss-public" "https://oss.sonatype.org/content/groups/public/"}

If you like following tutorials try the user/types guide. If you just want to get your hands on some typed code, see the Example project.

core.typed User Guide

core.typed Types Guide

Example project

API Reference

core.typed Github Home

core.typed Wiki

Please report bugs, ask questions or discuss things on the mailing list.

(FWIW I'm ambrosebs on #clojure.)

Thanks,

Ambrose

[Allen Rohner]

Awesome. Thanks for your hard work! 

Allen

[Ambrose Bonnaire-Sergeant]

Hi Daniel,

It is unsound to assume we can pass anything to an unannotated, unchecked var.

core.typed makes the user explicitly mark unchecked vars, which is also a source of unsoundness, but an explicit one. Hopefully :no-check is not ambiguous in this regard.

Take this example.

;; untyped namespace

(defn evil-atom-reset! [a]

  (reset! a :foo))

...

;; typed namespace

(defn nice-typed-fn []

  (let [a (ann-form (atom 1) (Atom1 Number))

        _ (evil-atom-reset! a)]

    (+ @a 2)))

If we simply assume evil-atom-reset! is of type [Any -> Any], our atom gets changed underneath us, and any type guarantees do not hold anymore.

The answer to this is generating contracts to wrap about our calls to untyped vars. These should probably be driven by user annotations though. Typed Racket automatically does this via macros, which is very cool, but probably impossible in Clojure.

So in general, implicitly trusting untyped code can be problematic. core.typed at least makes the user be explicit about unchecked vars so there is some chance the annotation is correct.

Thanks,

Ambrose

On Thu, Aug 29, 2013 at 12:06 PM, Daniel <double...@gmail.com> wrote:

Excellent work. I noticed that function parameter types default to Any when not Annotated.  What was the reasoning behind not mirroring this behavior for vars, and instead requiring an annotation?

--
--
You received this message because you are subscribed to the Google
Groups "Clojure" group.
To post to this group, send email to clo...@googlegroups.com
Note that posts from new members are moderated - please be patient with your first post.
To unsubscribe from this group, send email to
clojure+u...@googlegroups.com
For more options, visit this group at
http://groups.google.com/group/clojure?hl=en
---
You received this message because you are subscribed to the Google Groups "Clojure" group.
To unsubscribe from this group and stop receiving emails from it, send an email to clojure+u...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.

[Ambrose Bonnaire-Sergeant]

I see optional typing as the opposite of mandatory typing. You don't need to pass a type checker to get a program semantics.

Typed Clojure offers a particular flavour of optional typing: gradual typing. My interpretation of gradual typing is some of your code is rigorously statically typed, some is untyped, and there is some mediator that handles the interface between the two. (Typed Clojure lacks the mediator atm). You need to be explicit about the boundaries between typed/untyped to make the most of the type system.

If you're providing a library, the implementation could be completely untyped, but you might have annotations for your API.

Admittedly I've been exclusively researching Typed Racket style type systems for awhile now, but I'm sceptical that the kind of type system you describe would be effective in finding bugs in your programs. It might find them, but error messages will probably be unpredictable and unreadable, and the type system would not have simple rules to get a namespace type checking like Typed Clojure/Racket does. (eg. assign types to top-levels and fn parameters.)

I'm fairly confident that if you use core.typed, you'll see it's not for everything, but that it can rigorously type check some isolated code, which is often a use case. There are tradeoffs here: the more flexible the type system is, the more complicated the rules are for what type checks, and there will probably be tradeoffs in the accuracy of the static type system.

Also knowing that you've applied a picky, accurate type checker such as core.typed on a large code base is a (valid) good feeling. It will take investment though. In my experience, writing static types for functions is similar to a code review, and probably makes you think about what your code is doing a little more.

Thanks,

Ambrose

On Thu, Aug 29, 2013 at 3:13 PM, Daniel <double...@gmail.com> wrote:

Couldn't occurrence typing catch the error in that example, since evil-atom-reset! can only return an atom wrapping a keyword?

I guess the problem I had is that the "optional typing" moniker seems misleading since it forces you to annotate vars.  I had visions of gradually assigning types to vars as it became evident that typing was needed as a pre-runtime guardrail based on how other developers were using my functions.  If I'm publishing a library then that's backward thinking, but in a team using core.typed it sounds useful... Only type what you need when you need to.

Don't mind me... Clearly I need to actually use the library before developing an opinion.

[Ambrose Bonnaire-Sergeant]

Hi,

Roughly 1/3 of clojure.core is annotated and comes included with core.typed. They are unchecked annotations.

https://github.com/clojure/core.typed/blob/master/src/main/clojure/clojure/core/typed/base_env.clj#L658

You can lookup types via cf at the REPL.

(clojure.core.typed/cf +)

;=> (Fn [clojure.core.typed/AnyInteger * -> clojure.core.typed/AnyInteger] [Number * -> Number])

Thanks,

Ambrose

On Thu, Aug 29, 2013 at 3:40 PM, Jozef Wagner <jozef....@gmail.com> wrote:

How about annotating clojure.core API. Is it needed, provided, optional?

[Ambrose Bonnaire-Sergeant]

Also you can add missing annotations via ann.

(ann ^:no-check clojure.core/+ ....)

Core vars observe the same rules as all vars: they must be annotated.

Thanks,

Ambrose

[Ambrose Bonnaire-Sergeant]

Just pushed 0.2.1 based on feedback from the video on HN.

https://github.com/clojure/core.typed/blob/master/CHANGELOG.md

Thanks,

Ambrose

[Ambrose Bonnaire-Sergeant]

Hi Shantanu,

CLJS support is planned but not current plans to work on CLR myself.

No leiningen plugins yet, FWIW I tend to add type checks to my unit tests like:

(is (check-ns 'my.ns))

Thanks,

Ambrose

On Sat, Aug 31, 2013 at 4:13 AM, Shantanu Kumar <kumar.s...@gmail.com> wrote:

Sorry for a late reply to the thread. This release is pretty cool. I haven't been following the development too closely, so I have two questions:

1. Is ClojureScript/ClojureCLR supported by core.typed? Or, is it planned?

2. Is there a Leiningen plugin that can help run the type checks from the command line?

Shantanu