Overall, the work described in this dissertation leads to the conclusion that it
appears to be both practical and useful to design and implement an optional
static type system for the Clojure programming language.
I'm a huge type safety fan (see http://roy.brianmckenna.org/) so this is pretty amazing. I'm definitely going to play around with Ambrose's work.
Had a quick look, it's really exciting that the algo.monads was almost completely type-checkable with this system.
Leaves me with a couple of questions:
Multimethods are untyped. Anyone able to comment on how often multimethods are used in idiomatic Clojure code?
Anyone know if this work could eventually allow protocols to become full type-classes (allowing dispatch based on return type of protocol methods)? Am I misunderstanding how protocols are compiled?
Hopefully the videos for Typed Clojure at Clojure Conj 2012 will be posted soon after the talk is given :)
My only fear is that optional typing would be less useful than optional untyping. When you have libraries that are untyped, they're a pain to use from a typed language. The other way around is not true.
Multimethods are an awesome feature, which I'm a big fan of, but they were lower on my priority list so I haven't got around to typing them. It's not clear how comprehensively they can be typed either, I comment about it in "Future work".
I don't know a lot about type-classes, but I'm doubtful that Typed Clojure could help make protocols like them. I would expect a whole different dispatch system would need to be designed. But that's mostly a hunch. Very interesting problem.
If you want to play around with this kind of stuff immediately, check out Typed Racket. The Typed Clojure implementation is in alpha and might not be very friendly yet :) That said, please try it out!
If you like this work you'll also like Typed Racket, on which it is based. Sam TH is the main author and his publications are here: http://www.ccs.neu.edu/home/samth/
The first thing I thought of while opening this article was Qi / Shen, an optionally typed Lisp which takes inspiration from the ML family of languages. http://www.shenlanguage.org/
Shen's dedication to providing functional concepts such as partial application really interests me, but I find Clojure's practical nature even more enticing. Perhaps Typed Racket and this type system for Clojure will provide the best of both worlds!
Shen is pretty amazing and is built with a type system in mind from the beginning. If you don't want the type system, just turn it off, in the middle of a REPL session if you want!
I am not sure about the motivation for this project but this article helps explain why some folks are interested in type systems as detachable (pluggable) components, separate from languages:
I've read a few of Gilad's papers - I just don't see how they can be practical in a world of third-party libraries (e.g. author A hates types, I like type-safety but I have to settle for none when I use that library).
This paper demonstrates an effective way of interfacing between typed and untyped code such that type errors can only happen at the boundaries - not within typed code.
I guess, but this seems like something that could become a best practice for library authors, and it'd be fairly trivial to retrofit or fork existing libs with annotations.
> Multimethods are untyped. Anyone able to comment on how often multimethods are used in idiomatic Clojure code?
Not at all.
Multimethods were Hickeys solution to polymorphism before the Haskell enthusiasts managed to preach the gospel of type classes to him. Today, they are more or less deprecated as a solution to a problem.
This is categorically false. Multimethods solve a certain problem "open arbitrary function dispatch". Nothing in Clojure aside from multimethods solves this problem. There are many projects that use multimethods to their great advantage, including, but not limited to:
This is really great, and immaculately put together. Recently though I've come across people who think that you need strong types when programming, and this is really weird to me. I think it has its place for sure, and is a great way to ensure you're being correct, but I also really like not having to mess with types on hobby projects and such for sure :D
I'll just note that any corrections are more than welcome, this is my first paper and I've got a lot to learn! Please send them to abonnairesergeant at gmail dot com.
One of the distinguishing features of a classic Lisp is that values, not variables have a type-tag and the type-safety checking is performed at runtime. Everything is a reference (a pointer), everything is a first-class object (could be passed anywhere), everything is an expression (uniform syntax).
Ironically, Clojure is, a Java in the land of Lisp. They broke the abstraction layers, mess up logic with implementation, introduce not just different kind of parenthesis, but redundant and irrelevant data-structures and ruined the magic of "everything is a list". Look what a classic 3-lines 'keep function became.)
Now you're just trolling. Clojure's immutable persistent data structures are one of the primary strengths of the language, and what I tend to miss most when I'm working in another language.
By this definition, only PLT Scheme has really kept the flame alive then, right?
A lot of Common Lisp implementations have gone forward with replacing a lot of underlying machinery with type-inference-driven compilation and parts to actually get performance out of modern hardware. I don't see a huge difference here, except that there is a big interop layer more firmly baked into the stdlib.
Lisp is not just some implementation, it is a well-balanced set of ideas and trade-offs, which together produced a natural programming language with several dialects.
Clojure, on the other hand, is just an implementation of a bunch of features.
All I'm trying to say is that Lisp is incomparable more harmonized and much more elegant creation that Clojure, which compared to Scheme or Arc, is, excuse me, an ugliness.)
Engineering a platform or product is seldom a pretty business. Ask the Yesod folks. It's only recently that anything like Conduits with Conduit's performance is finally finding "good" and well-researched alternatives.
Not that your complaint is incorrect, it's just sort of difficult to actually use this as the basis for an argument against Clojure because everyone has already made their peace with this. It is not a "pretty" lisp; it's a natural response to the question, "How can I keep working with the JVM and leverage JVM libraries without devolving into the 1990's Taligent style verbosity that is modern Java?"
It's a different, weaker level of type safety that's become so prevalent that you probably take it for granted. The runtime checking is just to make sure that operations are performed on logical types.
My favorite analogy for this is the restaurant one. Haskell insists on having two waiters: one to deliver the food and a second to deliver the check. Clojure allows one waiter to deliver both, but throws a fit and leaves the restaurant if the check arrives before the bill. Assembler eats the first thing that arrives and signs the second, even if the bill comes before the food.
Clojure is "type-safe" in that it will exit instead of performing an illogical action (e.g. dividing a string pointer by a network socket). It's just as type-safe as Haskell code littered with fromJust.
What you're talking about now is totality. Both Haskell and Clojure allow non-total functions (functions which may not return a result) - the checking that they do are to stop undefined results. Agda is an example of a language that only allows total functions.
Adding the fromJust Haskell argument seems to have confused the argument I was trying to make. I had two points. The first one was better expressed by Evbn and I don't really have anything to add to that.
The second was that Clojure arguably has a type system. There is exactly one type, Stuff. Every function takes Stuff and returns Stuff. Of course, functions themselves are a kind of Stuff. Now, it lacks totality, but otherwise every compiled Clojure program has passed the type checker. It's just that type checking is a no-op, since there's no way for anything to have the wrong type.
Totality is different. In C you can (using a pointed cast cast) add a float to an intended and get gobbledygook (by interpreting the bits in memory incorrectly) and keep going. In Closure you can't, it will throw an exception, but you won't get warned about that until runtime.
Your example is nonsense. Clojure's keep is based on lazy sequences instead of concrete lists, and is also optimized for performance.
That said, you raise a point that occurred to me recently, and it relates to Clojure's literal representation of data beyond lists and your point about the "ruined magic".
In most Lisps, the only evaluation semantic is that of the "operator form": a list of operator car and arguments cdr, both of which are evaluated themselves.
Clojure, however, adds an evaluation semantic for its data literals. Consider this code:
{(+ 1 2) (+ 3 4)}
It results in the map {3 7}, but where is the "operator form" that caused the top-level evaluation?
In Lisps with reader macros, an expression like above boils into code resembling (hash-map (+ 1 2) (+ 3 4)), a classic "operator form", which is then evaluated.
In Clojure, however, which does not provide reader macros, there is no intermediate list representation of the expression accessible to the programmer. Effectively, Clojure adds evaluation semantics to Lisp beyond "operator forms": data literals evaluate their contents, and qualify in many ways as "special forms".
I have run into at least one implication of this design having to do with the structural representation of Clojure code. With a "classic" Lisp, an IDE or editor is empowered to present to the user any representation of the code, and can convert it to Lisp expressions arbitrarily the same way reader macros do.
With Clojure, this type of "skinning" is harder, because IDE-like navigation of data implies ordering. The ordering exists in the character-wise representation of a map like {3 4} but not in its evaluated counterpart.
My point is that they desugar directly to data structures (instantiated in Java, in LispReader) instead of operation forms that evaluate to data structures.
The implementation of Clojure itself is not idiomatic nor is it intended it to be so. Most of the complexity in that example, for instance, is to deal with chunked lazy sequences. In user-land code, chunking of lazy sequences is pretty much a pure performance optimization that you don't have to worry about.
Granted, it's not a ideologue "turtles all the way down" LISP. But it isn't intended to be. If you want that, I advise you to find an old Lisp Machine and use that.
Is the classic one actually going to be able to leverage tail-call elimination? Obviously it could be refactored to make a tail-recursive call, but correct me if I'm wrong, it wouldn't be automatic.
After refactoring it, the tail-recursive version would be a bit harder to read than the naive implementation. In a sense the Clojure code is in the same boat, it's just that the optimizations are more complicated, because it's not working with singly linked lists in the "address register" and "decrement register".
Because you then don't need the complexity (& boilerplate) of SERIES or LOOP the moment you want to do a series of transformations on a slightly bigger list.
You could write the clojure version in the exact same way (well, you wouldn't say null?, but, basically the same) as the lisp one. But it wouldn't be as efficient given the various ways sequences might be implemented in Clojure. That makes sense as part of the standard library, IMO---users of keep don't need to care about whether their sequence is chunked or whatever. And it makes sense that there should be a variety of implementers of sequences: there's more to life than singly-linked lists.
(Even Guy Steele, who should know, recommended a couple years ago that language designers omit cons from their langauges!)
I'm a huge type safety fan (see http://roy.brianmckenna.org/) so this is pretty amazing. I'm definitely going to play around with Ambrose's work.
Had a quick look, it's really exciting that the algo.monads was almost completely type-checkable with this system.
Leaves me with a couple of questions:
Multimethods are untyped. Anyone able to comment on how often multimethods are used in idiomatic Clojure code?
Anyone know if this work could eventually allow protocols to become full type-classes (allowing dispatch based on return type of protocol methods)? Am I misunderstanding how protocols are compiled?
Hopefully the videos for Typed Clojure at Clojure Conj 2012 will be posted soon after the talk is given :)
My only fear is that optional typing would be less useful than optional untyping. When you have libraries that are untyped, they're a pain to use from a typed language. The other way around is not true.