A Practical Optional Type System for Clojure

http://cloud.github.com/downloads/frenchy64/papers/paper.pdf

by swannodette • 14 years ago

164 51 14 years ago

cloud.github.com

th0ma5• 14 years ago

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

Anyway, great paper.

ambrosebs4• 14 years ago

Thanks, I intentionally chose examples where types are particularly useful, like monads and conduits (and apparently null elimination).

Evbn4• 14 years ago

I love strong types on hobby projects, so I don't have to constantly go back and fix crash bugs after I get it working once.

jshen• 14 years ago

You must be doing it differently than me, and most other people I've worked with.

pufuwozu4• 14 years ago

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.

firlefans3• 14 years ago

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:

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.175...

pufuwozu4• 14 years ago

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

noelwelsh• 14 years ago

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/

chadzawistowski• 14 years ago

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!

Tuna-Fish• 14 years ago

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

fogus• 14 years ago

> Not at all.

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:

* Clojure

* ClojureScript

* ClojureScript One

Rayne2• 14 years ago

They are not even remotely deprecated.

ambrosebs4• 14 years ago

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!

dschiptsov7• 14 years ago

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

dustingetz• 14 years ago

> They broke the abstraction layers, mess up logic with implementation

your opinion is one i haven't seen before, do you care to elaborate?

dschiptsov7• 14 years ago

http://news.ycombinator.com/item?id=4517540

pufuwozu4• 14 years ago

type-safety checking is performed at runtime

That doesn't really make sense to a type theorist. The definition of "type-safety" is only applicable statically.

What checking is done at runtime?

rprospero2• 14 years ago

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.

lukev2• 14 years ago

> but redundant and irrelevant data-structures

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.

dschiptsov7• 14 years ago

It is not about collections, it is about breaking the conceptual unity of the core language by using [] for a parameter.. array.)

gfodor2• 14 years ago

nice troll, but in clojure everything is a seq.

Rayne2• 14 years ago

That isn't actually true. Vectors, maps, etc, are not seqs. You can get a seq view of them, but the collections themselves are not seqs.

KirinDave2• 14 years ago

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.

dschiptsov7• 14 years ago

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

wooby2• 14 years ago

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.

lucian19002• 14 years ago

All of Clojure's literals desugar to calls. They're reader macros you can't add to.

ambrosebs4• 14 years ago

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.

A Practical Optional Type System for Clojure

Related Stories