Hacker News new | past | comments | ask | show | jobs | submit login
Why we're supporting Typed Clojure (circleci.com)
212 points by pbiggar on Sept 27, 2013 | hide | past | web | favorite | 73 comments

The paper behind Racket's new contract system which allows optional typing to be determined at runtime or compile time or both and across modules:


That's insane.

For a very long time I've regarded Racket as a purely educational Scheme dialect not particularly useful for real work. It was only a few months ago that I actually bothered to look at it's (amazing!) documentation [1] and realized how wrong I've been. It's incredible what are the Racket guys doing and what they've already achieved. The Typed Racket [2, 3] is "only" a cherry on top.

[1] http://docs.racket-lang.org/

[2] The Type Racket Guide: http://docs.racket-lang.org/ts-guide/

[3] The Type Racket Reference: http://docs.racket-lang.org/ts-reference/

What I see is that in part the transition from MZscheme to Racket has meant that a new generation of Lisp oriented academics are in PLT leadership roles - this is something Felleisen has long promoted in his own work (e.g. listing junior authors first on joint papers since everyone already knows who he is).

In other words, Racket is now being driven by research into computation and the earlier generation's area of emphasis - the pedagogy of computation - is being treated as a largely solved problem. This is not to say that PLT is no longer pursuing pedagogical projects or that in the past there wasn't significant discovery and invention within computation, only that the How to Design Programs project offers a mature and battle tested framework for teaching introductory programming and there is not a lot of reason to revisit it.

One of the things that attracts me to Racket - beyond the fact that it is a Lisp - is that the documentation is full stack. I was aware of the paper because there is a link within the Racket documentation of the contract system. The payoff from reading a paper that is specifically organized around the language at hand is intellectual continuity and when the language is a Lisp that continuity extends all the way from implementation to the lambda calculus.

I suspect it is done with higher order functions in a manner analogous to what Rich Hickey has done with map and reduce here:


One of the best ways to get people to support optional typing in dynamic languages is to make sure their tools can read those types and provide metadata.

Program verification is cool, but enabling "intellisense" on a hash is even cooler.

Indeed. I'm hoping the IDE support will include emacs - it can already do loads of cool things connected to nrepl, but completion on a hash would be amazing.

Does emacs support language aware intelliense (auto complete) for any language? I thought the common case was support through CTAGs.

I know of two modes for OCaml: TypeRex[1] and Merlin[2]. I've used both, and they both work reasonably well. The problem with TypeRex is that it requires changing your build, so it's not an easy option for companies that have some sort of custom build system in place.

Happily, by the time I got around to working at a company like that, somebody had written Merlin which does not need anything like that. It even worked with js_of_ocaml, which was very impressive. I thought it was a very good tool.

[1]: http://www.typerex.org/

[2]: http://kiwi.iuwt.fr/~asmanur/blog/merlin/

Emacs also has good support for a few other languages. Haskell has ghc-mod[3] and scion[4], for example.

[3]: http://www.mew.org/~kazu/proj/ghc-mod/en/

[4]: https://github.com/nominolo/scion

Similarly, there is ENSIME[5] for Scala.

[5]: https://github.com/aemoncannon/ensime

You can also use eclim[6] with Emacs, which integrates with Eclipse to offer rich functionality for Java.

[6]: https://github.com/senny/emacs-eclim

Of course, Emacs has language-aware editing for Emacs Lisp by default :). You can get similar support for most other popular dynamically typed languages as well.

So yes, Emacs does support plenty of languages like that, although almost always through a plugin. Happily, with the new package manager, installing and managing plugins is now trivial.

Yes, at least in clojure and CL. In Clojure, you use nrepl. Emacs (and several other IDEs) have clients which open a socket connection to your running clojure process. While editing a function, emacs will say "tell me about `my.namespace/foo`". It then shows arity and argument name info for the fn.

It's basically the same UX as you're used to in Java, except the info comes from asking the running process, rather than parsing statically.

It does for several languages (Dylan, Common Lisp, Java, etc). If you've got a compiler with an API, like say Clang, you can talk to it from Emacs Lisp.

How does Emacs plug into a statically typed language like Java? Does a compiler like Clang have an interactive/heuristic based mode suitable for use in a language-aware editor? Or do they just assume the code is in a good state and run the compiler when feedback is desired?

A compiler designed to support things like code completion can have an explicit API. For example, it may be asked to parse the code until the cursor location, the do a longjmp back out (or throw an exception, or whatever) with symbolic information about that location in the code.

If the parser error recovery is decent (and there is some effort put into this in most substantial front ends, since it's key to good error messages in large projects with long compile times, where recompile on every error fix isn't a great experience), the code doesn't need to be in a good state.

That might work...but does it work in practice (i.e. do you have an example where this is being used?).

I've found that most IDEs support two kinds of compilers: the compiler used to generate code and find type errors, and a "presentation" compiler to provide interactive feedback that is error tolerant and can run in incomplete contexts. Java works this way, Scala worked this way (at least when I was working on the plugin), C# has a lot of infrastructure separate from the compiler to support its use in Visual Studio. A lot of work goes into this infrastructure beyond "writing a decent compiler," and emacs very simple language-aware interface didn't seem to support it very well (when I looked ~8 years ago).

See: http://www.skybert.net/emacs/java. With Java, Emacs can just talk to the Eclipse Java Compiler, since it exposes an API. Same thing with Clang--it exposes an API which is used by XCode to support interactive feedback, and Emacs can consume it too. The Open Dylan compiler was originally intended to interface tightly with the Open Dylan Windows IDE, and that interface has been repurposed to interface with Emacs.

Cool, are these APIs buffer based or area based? I mean, when you make a change, do you get the message: the buffer has changed, or is there an area-based damage-repair cycle as in Eclipse or Visual Studio?

That might work...but does it work in practice (i.e. do you have an example where this is being used?).

It is how the Delphi compiler works in the IDE. I used to work for Borland, then Embarcadero, on the compiler front end.

When the compiler is running for code completion (kibitz mode, it calls it), it does a lot less work. No codegen, no type analysis of function bodies (begin / end blocks are entirely skipped), unless the cursor location is discovered to be inside a function body, whereupon the it rewinds and does more complete analysis. Normally takes no more than a few milliseconds to finish.

Yes, you can make it work for at least Java (JDE, I think?) and Python (I forget the mode, it's to do with Pymacs).

What is intellisense on a hash?

Autocompletion on the keys of a hash.

I know that in several communities, "hash" and "hash map" are synonymous. However, in Clojure hash maps are only one of several map implementations. We have implementations backed by linear array scans, prefix trees, and other data structures too.

The word "hash" a shorthand for the noun-phrase "hash code" (aka "digest") and a verb for the process of creating hash codes.

Oops. Sorry about that; I was still thinking in Ruby (day job) mode!

Oh right, a hash map. That would be very cool, and probably feasible to implement.

I still don't think this is worth supporting if you don't use Clojure. As far as dynamic languages go, I already use Racket quite a bit and as mentioned I can just use Typed Racket if I want, or I can use Racket's excellent contract system for some things (sparingly if I need good performance). Also I doubt it will catch on in the Python community, which is hostile to this sort of thing. JavaScript is perhaps a good use for it but there are already typed languages that run in the browser.

FWIW I've been pushing Typed Clojure in interesting directions that can be directly applied back to Typed Racket. The implementations are so similar that there is good potential for cross pollination.

Fair enough, it does sound like an interesting research project, I'm just not sure what will come of it. Can you make any speculations about what those directions might be? Or is it too early? Edit: global type inference? I thought that was infeasible for TR and Clojure at the moment?

Speaking speculatively, improving type inference is a great place for collaboration.

Concretely, I've extended several minor ideas.

Typed Clojure uses occurrence typing in sequential forms, as well as conditionals: http://frenchy64.github.io/2013/09/08/simple-reasoning-asser...

We can type check (filter identity coll) a little more accurately (which is actually quite hard to do): https://github.com/clojure/core.typed/blob/master/src/main/c...

The type system's interaction with Java's type system is interesting, which is something I've fleshed out.

I have heterogeneous maps as well as heterogeneous vectors, and support complex operations like merge. Unsure if relevant to Racket.

There are lots of other ideas which I need to implement to type check Clojure, but aren't necessarily crucial to type checking Racket, but would be nice to have.

Also I'm not aware of a tool to "guess" top level annotations for Typed Racket. This is an area I want to explore further, soon.

One of the TR maintainers (samth?) told me on IRC a while ago that it is very infeasible to do global type inference (top level) for TR. So I'm not sure how much you could get done in so short a time.

Yep that's correct. I want a tool that infers a rough approximation of top-levels to accelerate the process of porting untyped code to be typed. The programmer would inspect the annotations manually and fix any inaccurate ones, and then run the type checker.

I'm far from an expert on this, but F# has no requirement for all forms to be explicitly typed, so I'm a bit puzzled as to why this is hard.

Typed Clojure's type system is too rich to avoid top-level annotations. It's a similar situation to Scala.

I believe it has to do with features like subtyping and method overloading which cause havok for global type inference. Found a paper here: http://ropas.snu.ac.kr/lib/dock/HoMi1995.ps

Typed Racket and Typed Clojure are major sources of inspiration/reference for typed versions of JavaScript like TypeScript and possibly future versions of EcmaScript.

Pleased to see Rich Hickey also supporting this. http://www.indiegogo.com/individuals/222990/activities

Typescript also uses 'gradual' typing. See http://siek.blogspot.co.uk/2012/10/is-typescript-gradually-t... - Siek is referenced in the original post, too.

Clojure's type system sounds more powerful than Typescript's though.

AFAIK Typescript is level 1 gradual typing. Typed Clojure is also level 1, but I'm aiming for level 3.

I guess Typed Clojure is more powerful than Typescript in a few ways, but it's more about how well the type system fits the language. I've never used Typescript, but it seems to fit nicely, with interesting tradeoffs.

This is great news for Clojure.

Based on my experience, dynamic languages without optional typing make large scale enterprise development unbearable.

Sure, one should be writing unit tests, but in the enterprise context those tests rarely do exist, or if they do, either don't test what they should or are so complex that invalidate any re-factoring taking place.

Do you have any experience with the inverse statement? That is, have you had a good experience with optional types in an enterprise context?

I'm curious how many runtime errors persist due to the optionality of the type system. Perhaps code standards requiring all "library" code to be typed would be a good balance.

Just kind of.

Most enterprise customers I have worked with, favour dynamic languages just for scripting tasks, while using static typed ones for the large scale projects.

By large scale, I mean, projects with at least three development sites, at least 30 developers, all the different set of skills. With lots of attrition.

The only time I saw it working, was in a project done with TCL, which lacks optional types, but everyone on team was a top developer, the team was small, and located on the same open space. So startup world, not enterprise.

An introduction to typed clojure (strangely missing from both the blog post and the IndieGoGo campaign):


People interested in optional types for Python may be interested in my @typ decorator that implements them: https://github.com/cabalamat/ulib/blob/master/debugdec.md


    @typ((int,float), ret=(int,float))
    def square(x):
        return x*x
Here the parameter x is an int or float, and so is the return type.

It doesn't currently let you compose types, but that wouldn't be too difficult to add, e.g. {str:int} could mean a dictionary whose keys are strings and values are integers.

That's okay, but that doesn't seem to help much to verify your type correctness before runtime, which seems to me to be a big part of the benefit of type checking. Also, what you'd really want is something that implements type variables like:

    @typ[A implements *](A, ret=A)
    def square(x):
        return x * x
But I don't know how you'd do that in Python.

BTW, your printargs looks pretty cool! I might just makes something like that for JS...

> that doesn't seem to help much to verify your type correctness before runtime

I don't think that's possible in Python.

> Also, what you'd really want is something that implements type variables

That is possible, you could check what the type of the incoming parameter is and then check that the return value is the same type. I'm not sure that there's an obvious syntax for saying this, but one could always send a string to @typ and have it parse some made-up syntax.

I suspect this would be a lot of effort and it would probably make sens to use a typed language, instead of trying to shoehorn it into Python. I invented @typ so I could quickly document the types in my functions, & with the added advantage that it catches some errors.

> your printargs looks pretty cool! I might just makes something like that for JS...

I look forward to seeing it.

This guy is a little too souped on optional type-checking. This has existed in erlang for years, in the form of dialyzer (which allows for compile time validation of complex nested data structures), and in any dynamic language a good developer is using pre-checks & post-checks (in the case of js) or a combination of tagged values and pattern matching to ensure type-checking at runtime.

It's a nice feature, but calling it "one of the biggest advancements to dynamic programming languages in the last few decades" is ignorant.

OP here. I do actually believe what I said.

Pre- and post-checks are of course possible, but I've rarely seen them used in practice. More importantly, they can't be used to provide any sort of correctness guarantee, which static typing can.

I'm not sure what you mean by tagged values and pattern matching - I know what those concepts are, but I think you're saying they're widely used by good developers? I have not seen evidence for this.

The reason I call it one of the biggest advancements is that it is actually being used in production, has low overhead (both in cognitive load and performance-wise), and actually handles the complexities of duck-typing. It shows that it is practical. (By contrast, Erlang is sufficiently different to most other dynamic languages, both in use case and semantics, that it is difficult to generalize from Erlang to say Python).

>Pre- and post-checks are of course possible, but I've rarely seen them used in practice.

I agree, I wish more people (especially Javascript developers) saw the value of pre (and post!) checking.

>The reason I call it one of the biggest advancements is that it is actually being used in production, has low overhead (both in cognitive load and performance-wise), and actually handles the complexities of duck-typing. It shows that it is practical. (By contrast, Erlang is sufficiently different to most other dynamic languages, both in use case and semantics, that it is difficult to generalize from Erlang to say Python).

This is fair, I just meant to point out that conceptually this isn't new, it's just a new implementation. Can you expand a bit on what you said about duck-typing?

So most type checking, especially in how people write pre- and post-checks, is of the form "is this an X", for example, "is this object an instance of the String class". In duck-typed languages, that's not good enough, because you're not passing an instance of a subclass of a string, you're passing "something that quacks like a string" (aka implements the necessary interfaces to act string-like).

So the type of an object in a duck-typed language is based on the functions and fields it has _now_, not its instance type. Since there is no name for that type, you cannot do "nominal" typing. Instead, you must use "structural" typing, which checks its structure. This is exactly what Typed Clojure does.

An example of how that works in practice, is you say that the 2nd parameter must be a map with one of the following configurations: a key named :foo and a key named :bar, both mapping to strings, or a key named :error, mapping to a string.

I will tiptoe carefully around the issue you're bringing up and point out that the styles of type checking provided by Dialyzer and Typed Clojure are pretty different.

Perl6 & Rebol are some other examples of dynamic languages which come with optional typing.

NB. And I believe Perl6 in certain cases will/can raise compile-time type errors.

There one thing that really stirred my interest:

nil isn’t allowed

If this really is what I think it is (a certain reference to a class can never be nil) then I am really excited. It never made sense to me that someone was able to call a function I wrote that really needed instances with nils instead, so I was forced to check and throw in case they did. It's just not clear and it leads to a lot of unnecessary checking or nil pointer exceptions.

nil is explicit in Typed Clojure, and it's a goal to statically avoid misuses of nil.

This rough screencast describes on aspect to the approach http://vimeo.com/55280915

Check out cobra, python inspired -- it already helped developers "realize how great optional typing can be in everyday code": http://cobra-language.com/docs/why/

Great language too if you're down with .NET.

> Typed Clojure is one of the biggest advancements to dynamic programming languages in the last few decades. It shows that you can have the amazing flexibility of a dynamic language, while providing lightweight, optional typing.

I'm sure there have been great advances. But you are showcasing this as if it was a completely new idea, even though PHP has been using it for a long time. Correct me if I'm wrong.

OP here. This is substantially different than what exists in PHP. I tried to hint about this when referencing "nominal" vs "structural" in the piece, but you can just about say "I expect the parameter to be this type" in PHP, which is substantially less powerful than this.

Gradual typing is not as radical, however, as a fully type inferred language, see:


I think we can go much farther in this area than we have with Hindley Milner. Of course, this is still research, but as long as you are claiming "biggest advance in the last few decades" I might as well just throw this out there.

You're correct. Sam Tobin-Hochstadt is the star of the show, and is given a mention in the article, along with his fantastic Typed Racket.

You're totally wrong. For one thing, PHP coerces WAY too much for any type system to be effective. That's just plain duck typing.

I managed to totally miss the claim that Typed Clojure uses ideas from PHP :/ I'm pretty sure there is no relation.

What do you mean?

I'd like to see your defintion of structural typing in PHP. (Hint: Not casts, not lots of manual gettype)

I don't have a definition, I just use the thing. That's why I'm asking, I'm not a computer scientist. Eg:

    $f = function helloAction(Http\Request $request) {
        $response = new Http\Response("Hello " . $request->query->get('name'), 200);
        $response->setMa // at this point the IDE will show a list of methods like 'setMaxAge($time)', because it knows its type
Now I can pass $f somewhere else, like this:

And the method can accept it like this:

    protected method someMethod($f) {} // no checks!
Or like this:

    protected method someMethod(\Closure $f) {} // only an argument of type Closure will be accepted.
So those are types for me. If you are asking for something like this:

    Response $r = new Response(...);
Then yeah, PHP doesn't have that. Though I don't know why we would want that, it's kind of redundant.

The redundancy can be alleviated by type inference, but it's also kind of nice. The 'Response' on the left is your expectation about what $r is, while the one on the right is your implementation of that expectation. The separation is very important.

Of course, in this example, it's silly and type inference would be used to ensure that you don't need to write the left side.

The advantage is that before running your code you can suss out much greater degrees of what your code "could possibly mean". The \Closure bit is a start, but it needs to fail prior to running to be statically typed. It also could potentially include much more information like (\Closure[Http\Request -> Http\Response]) and reject even more bad arguments.

Pretty sure those are runtime contracts, not static types. Also see https://en.wikipedia.org/wiki/Structural_type_system

The type system for typed closure is much more powerful and is build on solid PL research. For example, it handles higher order types, union types and has a nifty system for overloading.

On this note, this doesn't seem to be more powerful than CL:s optional typing, am I wrong?

There is already typing in Clojure (and Python and Ruby). It`s called "100% unit test coverage". If you want it, you can have it now.

Can 100% unit test coverage give you intellisense, real-time warnings, and refactoring capabilities? Nope.

Unit testing is great for verifying that a piece of code works conforms to specification, but typing verifies that you're using a piece of code as expected. Two different things.

Unit test coverage (as much as I enjoy it, since that's how CircleCI makes all its money) is good, but it can't provide the guarantees static type checking can. Each has its place, and neither replaces the other.

Coverage isn't the same as enumeration of all possible modes. 100% test coverage might mean that all of your "wiring" fits together, but with dynamic languages it may not as runtime information may affect your types and break things.

100% enumeration of runtime behaviors is another property, far stronger than any non-dependent static types today, but also exponentially more difficult than 100% test coverage.

Good static types are a cheap way to get probably halfway between those two on a log scale.

I write lots of Ruby, and I downvoted you because this isn't very constructive.

100% of what? The parameter value space?

Registration is open for Startup School 2019. Classes start July 22nd.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact