[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

[Daniel]

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?

[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

--
--
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.

[Jozef Wagner]

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

[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

[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

[Nils Grunwald]

Congratulations and thanks for your work!

On Thursday, August 29, 2013 12:28:35 AM UTC+2, Ambrose Bonnaire-Sergeant wrote:

[Christian Sperandio]

Is there any perf improvement to use static typing in Clojure? 

Like we can see with Groovy 2.x and its static mode.

2013/8/29 Nils Grunwald <nils.g...@gmail.com>

--

[Michael Klishin]

2013/8/29 Christian Sperandio <christian...@gmail.com>

Is there any perf improvement to use static typing in Clojure?

core.typed is not a compiler, it's a type annotation/checker implemented

as a library.

If you are familiar with Erlang, it is to Clojure what Dialyzer is to Erlang.

--
MK

http://github.com/michaelklishin
http://twitter.com/michaelklishin

[Christian Sperandio]

Ok...

Another question, the checking is done only once (while compiling) ? Or, it's done while the runtime?

2013/8/29 Michael Klishin <michael....@gmail.com>

--

[Ambrose Bonnaire-Sergeant]

With Clojure the lines blur between compile time and runtime.

The clearest way to put it is that type checking is explicitly called at the REPL or in a unit test. Usually this is done during development iterations or testing time.

Re: performance improvements: Michael is correct. Interestingly Typed Racket offers numeric optimisations, but leans heavily on Racket's metaprogramming facilities to insert them automatically. There's potential in Typed Clojure for *identification* of speed improvements, but not actually inserting them. Typed Racket's "optimisation coach" comes to mind in ways we can present this information ("put a type hint at line 10, col 20 to get full speed...").

Thanks,

Ambrose

[Daniel]

If you can do that, why not return the literal representation of the type hinted function?

For the repl you could provide a function that interns the type-hinted function into the namespace by evaluating the literal representation first.

From there it's easy to provide something like slamhound.  Once you're certain types have been provided to your namespace correctly at the repl, run 'lein type <namespace>' to type hint everything in the namespace by literally restructuring the file.

Things type hinted with expressions would be tricky, but this could work (or you could just leave it alone):

myfn (original)

myfn-int

myfn-long

myfn-float

etc....

[Ambrose Bonnaire-Sergeant]

I don't think it would be possible to reconstruct the original forms in general, you would need to reverse macroexpansion to provide a form that has at least a passing familiarity with the original form. Otherwise you would get fully macroexpanded forms.

That's a lot of work!

[Daniel]

Those forms won't be in the namespace you're evaluating?

Yeah, it's probably a lot of work, but it sounds neat.  :-)

[Ambrose Bonnaire-Sergeant]

Well I'm sure people wouldn't be happy if their call to (+ a b c) was suddenly turned into (clojure.lang.Numbers/add (clojure.lang.Numbers/add a b) c)

:)

[Maik Schünemann]

On Thu, Aug 29, 2013 at 5:01 PM, Ambrose Bonnaire-Sergeant
<abonnair...@gmail.com> wrote:
> Well I'm sure people wouldn't be happy if their call to (+ a b c) was
> suddenly turned into (clojure.lang.Numbers/add (clojure.lang.Numbers/add a
> b) c)
>
> :)

the expresso [1] optimizer can be used for those optimizations ;)


[1] https://github.com/clojure-numerics/expresso

[Alex Baranosky]

Imo, there's nothing "easy" about writing something like Slamhound. Even after many iterations it can't handle macros, because ultimately they're impossible, without some kind of hints specifically added for Slamhound (or for Typed Clojure) :)​

[Daniel]

Yeah, it's pretty much impossible unless you limit yourself to a manageable subset of Clojure.  The "easy" part I was referring to was the Leiningen plugin, not the whole kit n' caboodle.

[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

[Shantanu Kumar]

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

[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