top | item 10271149

Why we’re no longer using Core.typed

122 points| dankohn1 | 10 years ago |blog.circleci.com | reply

145 comments

order
[+] arohner|10 years ago|reply
I introduced core.typed to Circle, and I was responsible for most of the early type annotations in the Circle codebase. Because of me, Circle was also the first large contributor to core.typed's kickstarter campaign.

Other commenters are speculating that this kind of tool needs to be built into the language, and planned ahead of time. IMO, this is completely wrong. core.typed fits surprisingly well into the language, and there are no fundamental reasons in Clojure or core.typed preventing it from working well.

I largely agree with the criticisms raised in the post, but it's worth pointing out that core.typed is developed by one guy, part-time while working on his phd. The problems are all related to maturity of the project, and bandwidth. core.typed's version number is currently 0.3.11, which gives you an idea of its state.

Ambrose has shown what is possible; I'm confident that with more help, core.typed can become an amazing tool for finding bugs in production code.

[+] dopamean|10 years ago|reply
> I'm confident that with more help, core.typed can become an amazing tool for finding bugs in production code.

This is true but I wonder how much Clojurists care about what core.typed offers. If not enough do then many there will never be enough contributors to really make it work. LightTable is a project that seems to have had something similar happen.

[+] grandalf|10 years ago|reply
thanks for posting this. Great to hear this perspective.
[+] wpietri|10 years ago|reply
Over and over I see reports of iteration speed being critical to real-world projects, and that's certainly my experience.

But it's something I rarely see featured in tool design. So many of our tools are still batch oriented: they start from scratch, read everything, process everything, and then exit. That made sense in an era where RAM and CPU were expensive. But now that they're cheap, I want tools that I start when I arrive in the morning and kill when I go home. In between, they should work hard to make my life easy.

If I'm going to use a type checker, I want it to load the AST once, continuously monitor for changes, and be optimized for incremental changes. Ditto compilers, syntax checkers, linters, test runners, debugging tools. Everything that matters to me in my core feedback loop of writing a bit of code and seeing that it works.

For 4% of my annual salary, I can get a machine with 128GB of RAM and 8 3.1 GHz cores. Please god somebody build tools that take advantage of that.

[+] jrochkind1|10 years ago|reply
The problems I've seen with tools that try to load everything once and monitor for incremental changes -- is it's hard to get RIGHT. These tools tend to be buggy, or worse tell you it's not them that's buggy, it's you that's "doing it wrong" somehow, trying to work the way you want.

The beauty of simple tools is it's easier to make simple tools that work really really well. From loading everything at once, to considering text editors vs "IDE", which is really part of what you're talking about too. When we have new languages and platforms all the time these days... it's important to be able to get high-quality tools that don't take forever to develop.

[+] spicyj|10 years ago|reply
Facebook's Flow and Hack typecheckers both do this.
[+] carterehsmith|10 years ago|reply
"Please god somebody build tools that take advantage of that."

Like, an IDE?

[+] jshen|10 years ago|reply
"iteration speed being critical ... But it's something I rarely see featured in tool design."

Go? They've always had this as a top level goal.

[+] jerf|10 years ago|reply
That... is pretty much exactly the list of problems I've expected out of optional typing.

I think other dynamic-type language communities should read this and think really hard. I've said before, I'd rather see a language become the best $LANGUAGE it can possibly be, for whatever that $LANGUAGE is, than try to bolt things on that pull it away from its core focus. Dynamically-typed languages are dynamically typed. Become the best dynamically-typed language you can be, don't bolt less-than-half-assed static typing on to the side. The sum ends up being less than the parts.

And if that means the next ten years is the language slowly fading into history... that is the destiny for all of us anyhow. Let it be with a fantastic dynamic language that was the best it could be, let it be a language that people speak wistfully of twenty years later. Don't make it be remembered as a Frankensteinien monstrosity as it tried to stay current.

[+] rurban|10 years ago|reply
Not at all. This is the list of problems that exist with an overly slow, early and incomplete type checker.

This has nothing to do with optional typing at all. It's just the expected problems with an early and slow (2min!) implementation of core.typed.

Other type checkers and inferencers in gradually typed languages don't have these problems, so you cannot generalize.

E.g. Optional types in Common LISP on which Clojure is based on doesn't have these problems. Scala has similar problems, but most other non-JVM based gradually typed languages not.

[+] fernandezpablo|10 years ago|reply
I disagree. Typescript is an excellent example of an optional static type system that works great. It has none of the 3 problems the OP describes: it's fast, it nicely encompasses the whole language and the Definitely Typed repository includes a TON of 3rd party library type definitions.
[+] erichmond|10 years ago|reply
Core.typed is a library, not an extension to the language itself. It's completely optional and is not related to clojure.core at all.

While your points may be valid, this may not be a great example.

[+] outworlder|10 years ago|reply
> I'd rather see a language become the best $LANGUAGE it can possibly be, for whatever that $LANGUAGE is, than try to bolt things on that pull it away from its core focus.

On the other hand, there are instances where types are useful, even in dynamically typed languages. One of them is optimizations. The job of a compiler gets much easier if it can assume that a given variable will always be, say, an integer and nothing else.

[+] drcode|10 years ago|reply
> don't bolt less-than-half-assed static typing on to the side.

To be fair, core.typed is a completely independent, optional library- It does in no way detract from the dynamic nature of the language or affect you in any way if you simply refrain from including it in your project.

[+] pron|10 years ago|reply
First of all, adding optional static typing is not "trying to stay current". You may be surprised (I certainly was), but at the last ECOOP it was very clear that the typed/untyped/optionally-typed debate is very much alive and well. Second, optional typing in itself is a hot topic (regardless of the merits of static typing), with some very interesting work. See, e.g. the extremely-powerful-but-not-yet-production-ready pluggable type systems supported by Java 8: http://types.cs.washington.edu/checker-framework/current/che..., or Gilad Bracha's optional types in Dart.
[+] oskarth|10 years ago|reply
Just to clarify, core.typed is just a library.
[+] swah|10 years ago|reply
Do you think optional typing could work if it was part of the language? Or the problems with it are intrinsic?
[+] numlocked|10 years ago|reply
I don't have nearly the breadth of experience in Clojure as the circleci guys, but I found that Prismatic's Schema [0] works well for me vs. core.typed. I can selectively annotate functions with their return types, and test runs will validate that they are returning as expected. It's runtime evaluated, so you lose a lot of static analysis benefits that type checking gives you, but it still provides some good code coverage, forces you to think about types a bit, and (the biggest benefit for me) it serves as documentation for functions that might return somewhat complex types. I can return to code months later and have a good idea of what's going on.

I've found the syntax a little arcane, particularly for coercion (which is a secondary function of Schema) but the documentation benefits have been worth the effort of learning it.

A nice middle ground between nothing, and full-blown type annotations.

[0] https://github.com/Prismatic/schema

[+] DougBTX|10 years ago|reply
Interesting to compare with TypeScript, which runs into similar issues.

Before TypeScript 1.1, the intelligence was quite slow, but is now fine even for large projects. Third party libraries often have type definitions in the DefinityTyped collection.

That just leaves constructs that work in JavaScript, but which can't be type checked in TypeScript. This is often double-edged. TypeScript's types are not amazingly flexible, so it encourages writing less magical code, improving readability, but it also discourages some patterns that are quite useful, such as passing references to properties using string key names, which are hard to type-check.

[+] aikah|10 years ago|reply
> TypeScript's types are not amazingly flexible, so it encourages writing less magical code (...)

you can "cast" anywhere so it's not really an issue :

(<(string)=>string>baz['baz'])('foo')

Otherwise typescript support union types and such ... Even without .d.ts headers everywhere it is still useful. I prefer it to babel and co as it is easier to track ES6/7 integration. Never used typed clojure though ,but I don't know any example of a language that didn't have types before and retrofitted type safety without any issue and breaking backward compatibility.

[+] muhuk|10 years ago|reply
I gave up on core.typed because I've found adding type annotations to most of the forms is significantly harder compared to a statically typed language. (In hindsight this is obvious, I know.)

Not having type-checking doesn't necessarily make Clojure any less awesome for me though. I write unit tests, add (some form of) contracts at least to the public functions and pay attention to documenting public stuff. And not doing excessively clever things like having unnecessary mini-DSL's within the code also help.

[+] TheAceOfHearts|10 years ago|reply
I feel like I can somewhat relate, I've been adding flowtype [0] annotations to my JS code, which is transpiled with babel. However, since I'm using unsupported ES2015 features and experimental ES2016+ features, it fails to run over my code (which is completely understandable).

The workaround I've found is to use a plugin [1], which converts the type annotations into runtime checks. It's not perfect, but I've found it helps catch some bugs quickly. It's also really helpful for documentation purposes: you know that this function param takes a number param, if you're not passing in a number you've made a mistake. Also, having the inline type is nicer than having it in a jsdoc-style comment above.

I think there's diminishing returns as you add more annotations to your code and you make them stricter, but having basic sanity checks has been helpful in catching stupid mistakes quickly.

[0] http://flowtype.org/ [1] https://github.com/codemix/babel-plugin-typecheck

[+] cwyers|10 years ago|reply
Why Flow instead of Typescript?
[+] j_m_b|10 years ago|reply
>In September 2013 we blogged about why we’re supporting Typed Clojure, and you should too!

I wonder how many other premature "you should too"s have been issued over the years. At least they had the guts to retract theirs.

[+] pbiggar|10 years ago|reply
I wrote that post, and it was very much about why you should support Typed Clojure, not why you should use it. You should support it for the potential, you should decide whether to use it on practical concerns.
[+] shadowcat|10 years ago|reply
"You should support this" is not the same as "we're using this". Typed Clojure was a neat research project (disclaimer: I supported it) but it seemed not to work for their actual needs.

Even though I no longer use Clojure much and prefer to work in languages designed for static typing (e.g. Haskell) I don't regret my donation. It is an ambitious project and I'm glad someone had the courage to take it on.

[+] lisa_henderson|10 years ago|reply
This bit raises the question, is #1 being caused by #2 and #3?

--------------------------------------------

The problems that we have hit with using Typed Closure are

1.) slower iteration time when programming,

2.) core.typed not supporting the entire Clojure programming language

3.) using third-party libraries that have not been annotated with core.typed annotations

--------------------------------------------

If #1 is caused by #2 and #3 then presumably #1 will get better with time. But if #1 is caused only by typing itself, then it sounds like, for them, using types was a bit of premature optimization.

It does raise the question, is it possible to create a type system that does not slow a project down?

[+] Gonzih|10 years ago|reply
But what about then gradual typing in core.typed? Will it make core.typed more useful? Or is problem not just in gradual typing but more in type oriented system vs data oriented system?
[+] Ovid|10 years ago|reply
The issue I have with gradual typing in most languages is that it's added after the fact and not native. As a result, the integration isn't native and you start seeing issues like this.

This, incidentally, is one of the reasons I like Perl 6 (http://perl6.org/). It also has gradual typing, but if a third-party library doesn't have a type annotation, that's OK: it will simply fail at run time instead of compile time.

Another reason to like native gradual typing instead of third party gradual typing is that it can be integrated natively into the system instead of being used as an afterthought. Perl 6 has native type infererence to allow for compile time failures:

    $ perl6 -e 'sub foo(Int $x) { say $x }; foo("bob")'
    ===SORRY!=== Error while compiling -e
    Calling foo(str) will never work with declared signature (Int $x)
    at -e:1
    ------> sub foo(Int $x) { say $x }; ⏏foo("bob")
(Yes, that's compile time instead of run time)

What happened above is that the optimizer saw that the call to foo() requires an Int and checks the argument type to see if the call is allowed.

And here's the untyped version:

    $ perl6 -e 'sub foo($x) { say $x }; foo("bob"); foo(3)'
    bob
    3
Interestingly, the Perl 6 core team could allow for powerful type inference with this, but one of the core issues has always been that many languages using type inference have rather opaque error messages because they essentially dump a "proof" of type failure and many struggle to understand them. Thus, the the Perl 6 devs are taking more careful approach, though they know they can do more. For example, this falls back to a runtime failure instead of a compile time failure:

    $ perl6 -e 'sub foo(Int $x) { say $x }; my $name = "Bob"; foo($name)'
    Type check failed in binding $x; expected 'Int' but got 'Str'
      in sub foo at -e:1
      in block <unit> at -e:1
In other words, because it's not sure of the type of $name at compile time, it falls back to run time (though in the simplistic example above, that's clearly not the case). Annotate the $name variable and you get a compile time failure again:

    $ perl6 -e 'sub foo(Int $x) { say $x }; my Str $name = "Bob"; foo($name)'
    ===SORRY!=== Error while compiling -e
    Calling foo(Str) will never work with declared signature (Int $x)
    at -e:1
    ------> t $x) { say $x }; my Str $name = "Bob"; ⏏foo($name)
With this, third-party libraries which don't declare types work just fine, but you get type-safe run time failures. If they do declare types, you often get compile time failures (though it will still fall back to run time, and won't check at run time if it knows at compile time that it works).
[+] Confusion|10 years ago|reply
Does anyone know how the situation is with typed Racket? Similar problems with speed, annotations being hard to write and tooling being insufficient?
[+] samth|10 years ago|reply
Typed Racket (due to different integration into the compiler) is much more incremental -- the speed issues in the blog post would be much reduced. The typechecker still isn't as fast as we would like, though, although we have plans to improve it.

I think the tooling integration is better in Typed Racket, although Ambrose has made some improvements in Typed Clojure as well. As for typed versions of existing libraries, I think that things are bit better in Typed Racket, but also Racket has many fewer libraries than Clojure at the moment, so the scale of the problem is smaller.

[+] MBlume|10 years ago|reply
It seems like something like the dependency tracking and selective reloading in Stuart Sierra's tools.namespace could be used to mitigate their first problem.
[+] agumonkey|10 years ago|reply
The code ahead types strongly remind me of the state of UML model driven trends a few years back. I wonder if it ended the same way.