Out of curiosity, did you try Typed Clojure? It certainly has its rough edges, but you sound willing to bear the burden of annotating code with types (at the top-level, at least) and I *think* its treatment of Java interop does what you want: unless instructed otherwise, the typechecker assumes that arguments to Java methods must not be nil and that any Java method may return nil.
On Thursday, October 20, 2016 at 8:39:04 AM UTC-4, Colin Fleming wrote: > > 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 <did...@gmail.com <javascript:>> > 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 clo...@googlegroups.com >> <javascript:> >> Note that posts from new members are moderated - please be patient with >> your first post. >> To unsubscribe from this group, send email to >> clojure+u...@googlegroups.com <javascript:> >> 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+u...@googlegroups.com <javascript:>. >> 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.
