6 ms·

A Practical Optional Type System for Clojure

164 points by swannodette 14y ago

th0ma5 14y 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.
- ambrosebs 14y ago
  Thanks, I intentionally chose examples where types are particularly useful, like monads and conduits (and apparently null elimination).
- Evbn 14y 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 14y ago
    You must be doing it differently than me, and most other people I've worked with.
pufuwozu 14y 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/ 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.
- firlefans 14y 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.1460&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.175...
  - pufuwozu 14y 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).
    - firlefans 14y ago
      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.
    - jamii 14y ago
      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. homepages.inf.ed.ac.uk/wadler/papers/blame/blame.pdf
- noelwelsh 14y 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/ http://www.ccs.neu.edu/home/samth/
  - chadzawistowski 14y 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/ 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!
dschiptsov 14y 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 14y 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?
  - dschiptsov 14y ago
    http://news.ycombinator.com/item?id=4517540 http://news.ycombinator.com/item?id=4517540
    - zcam 14y ago
      Apple & oranges. The only thing these 2 have in common is their name, the clojure version does a lot more. A definition of a similar keep fn in clojure would be almost indistinguishable from your lisp example (it would just be more readable).
      - dschiptsov 14y ago
        Who told you that more is better? Why we should have nested lets and all that boilerplate for a classic filter?
        simonb 14y ago
        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.
ambrosebs 14y 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.

164 points by swannodette 14y 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.

ambrosebs 14y ago
Thanks, I intentionally chose examples where types are particularly useful, like monads and conduits (and apparently null elimination).
Evbn 14y 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 14y ago
  You must be doing it differently than me, and most other people I've worked with.

pufuwozu 14y 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/ 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.

firlefans 14y 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.1460&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.175...
- pufuwozu 14y 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).
  - firlefans 14y ago
    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.
  - jamii 14y ago
    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. homepages.inf.ed.ac.uk/wadler/papers/blame/blame.pdf
noelwelsh 14y 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/ http://www.ccs.neu.edu/home/samth/
- chadzawistowski 14y 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/ 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!

dschiptsov 14y 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 14y 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?
- dschiptsov 14y ago
  http://news.ycombinator.com/item?id=4517540 http://news.ycombinator.com/item?id=4517540
  - zcam 14y ago
    Apple & oranges. The only thing these 2 have in common is their name, the clojure version does a lot more. A definition of a similar keep fn in clojure would be almost indistinguishable from your lisp example (it would just be more readable).
    - dschiptsov 14y ago
      Who told you that more is better? Why we should have nested lets and all that boilerplate for a classic filter?
      - simonb 14y ago
        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.

ambrosebs 14y 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.