I recently spent a bunch of time researching exactly this. My motivation was that my main project, Cursive, suffers from a ton of NPEs which I find very difficult to manage. I wanted to see how difficult it would be to have a typed Clojure-like thing, using something similar to Kotlin's type system. Kotlin uses a type system which is similar to Java and has Java interop as a primary goal, which I would also need since Java interop is essential to me. It fixes a bunch of flaws in the Java type system and adds new features like nullable types, which I now find it difficult to live without.
Before anyone asks, spec is not useful for me because it relies heavily on generative testing to increase your confidence in your functions. I can't use generative testing because my application is tied to a large Java codebase which I cannot model to any useful degree. Essentially, spec recommends runtime tests at the boundary of your system, and nearly my entire system is interop boundary. I'm not interested in runtime checks except where absolutely necessary - Kotlin does this for me transparently, spec doesn't. Here's a short list of my findings. I'm happy to expand on any of these points if anyone is curious. It bears repeating - Java interop is non-negotiable for me, and that makes a lot of this harder than it would be otherwise. Disclaimer: I'm no programming language expert. This was hard for me, and a surprising amount of it was new to me. I'd appreciate any corrections or clarifications. 1. Type systems are hard. I for one didn't appreciate the complexity that goes into making them easy to use. Don't be fooled by the 20-line implementations of Hindley-Milner. 2. In particular, generics are very hard, and variance for generic objects (i.e. the intersection of generic objects and OO) is the source of much difficulty. 3. Type systems are split into two main camps - nominal typing (like Java, where the types are identified by names) and structural typing, where the type of an object is defined by it's "shape", like Go's interfaces. 4. One of the major benefits of Clojure is its heterogeneous collections, a.k.a. "just use a map". This is very difficult to maintain in a type-safe manner without losing most of the benefit. 5. There are two main things I was interested in from a type system - type checking (i.e. making sure that your program's types are correct) and type inference (working out what the types of things are from the code, so you don't have to annotate everything). Type checking is relatively straightforward, but type inference can be very hard indeed. 6. Much of the complication comes from the need to interop with Java. ML-style interface essentially doesn't work if you want to maintain compatibility with Java since it cannot be interfaced in a useful way with nominal OO systems. In particular, method overriding is basically impossible to represent. 7. #6 implies that you cannot have a language with good Java interop *and* global type inference, i.e. you will definitely be annotating your function parameter types, and your function return types. I'm ok with this since IMO it's a good practice anyway. 8. Once you start thinking about the fact that you no longer have heterogeneous collections, and start thinking about what the alternatives would look like, you start to realise that you'd end up with basically the ML family style of data types - homogeneous collections, typed tuples and ADTs. I'm actually ok with that too, since they're a very nice set of primitives and I think they probably represent 95% of how people use Clojure's collections anyway. 9. Structural typing seems like it might be a good fit for something like Clojure's maps. However, mixing structural and nominal typing *and* OO seems to be the path to madness. I think that's it. This is still a project I'd like to tinker with at some point, but I think it's fair to say that I dramatically underestimated the amount of work a useful Java-compatible type system would be. I still think it seems like a nice point in the language design space though, which is curiously unfilled on the JVM (some of you may have noticed that I basically want F# with nullable types). Cheers, Colin On 16 October 2016 at 00:14, Didier <didi...@gmail.com> wrote: > I know a lot of people like to say how unhelpful Java like static typing > is, and only more powerful type systems of the ML family add value, but > I've been wondering recently if for Clojure it wouldn't make more sense to > simply extend the type hints to enable an optional Java like static typing > scheme. > > It is my understanding that ML style static typing is incredibly difficult > to add properly and without compromise to a dynamic language. That doing so > limits the scope of type inference, rendering the task of adding type info > more tedious then in ML languages themselves. > > ML style static typing provide enhanced safety grantees, but seem to add > too much complexity to Clojure to be practical. What about a Java like > static typing scheme though? > > I haven't found in practice that the safety of Clojure was an issue, as > the REPL workflow tend to promote quite a lot of testing. So I'm not too > worried about needing the state of the art of provable correctness for my > programs. What has been a biggest cause of issue to me was refactoring and > shared code base across a team. Those last two use cases are actually > pretty well handled by Java like static type checking. Is it a powerful > type checker, not really, but it enables most trivial type errors to be > caught early, and it allows easier integration points for other devs to > follow, as well as documentation for functions, better tools support and > easier refactoring, while also enabling performance optimizations. > > I have limited knowledge in typing systems, and have no idea how easy it > is to implement them, but as a user of Clojure, I feel like I would find an > optional Java like static typing a great addition, one that I am more > willing to use and benefit from then Typed Clojure's more complex ML style > type checking. > > What do other think? > Can anyone with better knowledge tell me if this would be feasible or if > adding such gradual typing system is effectively as hard as adding ML style > type checking? > > -- > You received this message because you are subscribed to the Google > Groups "Clojure" group. > To post to this group, send email to clojure@googlegroups.com > Note that posts from new members are moderated - please be patient with > your first post. > To unsubscribe from this group, send email to > clojure+unsubscr...@googlegroups.com > For more options, visit this group at > http://groups.google.com/group/clojure?hl=en > --- > You received this message because you are subscribed to the Google Groups > "Clojure" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to clojure+unsubscr...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > -- You received this message because you are subscribed to the Google Groups "Clojure" group. To post to this group, send email to clojure@googlegroups.com Note that posts from new members are moderated - please be patient with your first post. To unsubscribe from this group, send email to clojure+unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/clojure?hl=en --- You received this message because you are subscribed to the Google Groups "Clojure" group. To unsubscribe from this group and stop receiving emails from it, send an email to clojure+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
