News for hackers. Stuff that matters.
Re:Kotlin: A Language with a Bright Future by pron on Friday December 01, 2017 @04:56PM (#15827968)
> If it were that easy we'd see a lot more people doing it.

It is that easy. What is hard isn't knowing JML, but gaining experience with specification in general. This is a skill that is required regardless of formalism (and is actually why Idris and Java+JML, despite being very different, are still much more similar than they are different; same goes for TLA+ and Lean).

One of the reasons I would encourage those who are interested in correctness to read Schmidt's overview of abstraction/refinement relations [1] -- which forms the core of possibly the most important idea in all of program analysis: abstract interpretation -- is that it allows one to see type systems, contracts, refinement logics etc. as different expressions of this same core idea; specifically of a Galois connection between different abstraction levels, be they a program and its type, a program and its contract, or different abstraction levels in a formalism like TLA.

> It's much harder without monads.

But you have monads in Java. In fact, there are many more Java programmers using monads (e.g., Stream and CompletableFuture) than Haskell and Scala programmers using monads combined. What you can't do is abstract over all monads, which is of questionable value even in Haskell (and Java has other ways of abstracting over common patterns).

The goal now is to remove the need for monads in Java. Monads are equivalent to delimited continuations, but delimited continuations compose more easily (algebraic effect systems are modeled after them) and they fit much more nicely with imperative constructs like loops and exceptions. Delimited continuations are the monads of imperative programming, and they are coming to Java.

[1]: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.4...

Re:Kotlin: A Language with a Bright Future by lmm on Monday December 04, 2017 @03:56AM (#15842568)
> But you have monads in Java. In fact, there are many more Java programmers using monads (e.g., Stream and CompletableFuture) than Haskell and Scala programmers using monads combined. What you can't do is abstract over all monads, which is of questionable value even in Haskell (and Java has other ways of abstracting over common patterns).

A broad library of standard functions is certainly valuable; working in Java with Stream and CompletableFuture one naturally finds oneself wanting traverse, cataM and dozens of other such helpers. Maybe the ability to abstract over monads is only useful to library authors, but the libraries they produce are then immensely useful for regular programmers.

> Monads are equivalent to delimited continuations, but delimited continuations compose more easily

Perhaps, but at the cost of completely incomprehensible code. We've known for years or decades that continuation-based style can produce higher-performance code than conventional approaches, but they've seen limited adoption even in high-performance environment; many, perhaps most programmers (myself included) just don't and can't "get" them.

Re:Kotlin: A Language with a Bright Future by pron on Monday December 04, 2017 @04:50AM (#15842745)
> one naturally finds oneself wanting traverse, cataM and dozens of other such helpers. Maybe the ability to abstract over monads is only useful to library authors, but the libraries they produce are then immensely useful for regular programmers.

I find libraries that help developers save a few lines of code here and there not worth changing a programming paradigm. By far the biggest boost comes from reuse-in-the-large. I fully agree that languages with such higher-order constructs allow writing more reusable code than classical imperative languages. But "more", in this case, does not translate to big savings and does not justify a change of paradigm. We are deep in diminishing returns territory there, even if pure FP had no disadvantages.

But those higher-order constructs do not require a pure language, and could be added to Java/Kotlin once there are no bigger-impact improvements to be made, and if it's judged that their meager contribution justifies adding complexity to the language. Not every added utility automatically translates to "we should do it." Its cost must be weighed as well. Languages like Java/Kotlin choose to be more conservative in the cost/benefit of the features they embrace compared to languages like Scala.

> Perhaps, but at the cost of completely incomprehensible code.

Quite the opposite. Ordinary imperative code (i.e., blocking threads) is programming with continuations. Continuations are the core abstraction of imperative languages, just as partial functions are the core abstraction of pure-functional ones, and all the core constructs in those languages -- loops, exceptions -- are built to work with them. The complex code you're thinking of is analogous to very complex code that can be achieved with monads. While it could be done, there is no reason to ever do it.

Re:Kotlin: A Language with a Bright Future by lmm on Monday December 04, 2017 @10:09AM (#15844343)
> I find libraries that help developers save a few lines of code here and there not worth changing a programming paradigm. By far the biggest boost comes from reuse-in-the-large. I fully agree that languages with such higher-order constructs allow writing more reusable code than classical imperative languages. But "more", in this case, does not translate to big savings and does not justify a change of paradigm. We are deep in diminishing returns territory there, even if pure FP had no disadvantages.

I find being able to reduce code in the small yields exponential returns in the large. If one can reduce the size of plain code by say 10%, making functions and classes shorter and easier to comprehend, then that takes some of them below the threshold where they need to be split up, and unlocks further opportunities to see and factor out commonality, reducing code size and class counts further. That might take you below the threshold for needing to separate a layer in the larger component, and that in turn allows more reuse; that might take a component below the threshold of needing splitting up, and that might take the project below the threshold where it needs multiple developers or multiple teams involved.

You don't have to change paradigm. I can understand (though I don't agree with) wanting more operational features in a language. But I can't understand being so hostile to these conservative but useful features.

> But those higher-order constructs do not require a pure language, and could be added to Java/Kotlin once there are no bigger-impact improvements to be made, and if it's judged that their meager contribution justifies adding complexity to the language. Not every added utility automatically translates to "we should do it." Its cost must be weighed as well.

Costs should indeed be weighed, but HKT has one of the strongest cases in terms of power-to-weight: it's a very cautious extension of the type system that doesn't really make the language any more complex, since it just means permitting type parameters to be used in ways that concrete types are already allowed to be used. And virtually every application can benefit; I use traverse virtually every day. Features like language-level null or delegation have a much higher risk (they change more of the rules of the language, a reader has to be aware of them even if they aren't using them directly and when they're not necessarily visible in a function signature) and are less broadly applicable.

> Quite the opposite. Ordinary imperative code (i.e., blocking threads) is programming with continuations. Continuations are the core abstraction of imperative languages, just as partial functions are the core abstraction of pure-functional ones, and all the core constructs in those languages -- loops, exceptions -- are built to work with them.

Threads, loops and exceptions are notorious sources of bugs and incomprehensible code. To the extent that they're the core of imperative programming, imperative programming is a bad thing.

Re:Kotlin: A Language with a Bright Future by pron on Monday December 04, 2017 @10:44AM (#15844677)
> I can't understand being so hostile to these conservative but useful features.

I am not hostile to them, just skeptical of their cost/benefit. I don't think every useful feature has a place in every language. Different languages should have different thresholds for the cost/benefit of features they want. It's perfectly legitimate for Scala to have a low threshold, and for Kotlin/Java to have a high one. In fact, a high threshold on cost/benefit is one of the cornerstones of the Java design philosophy, as laid down by James Gosling back in the 90s. He said that his design philosophy for Java specifically excludes features that are just a good idea, and only includes features that solve major problems (of course, what constitutes a major problem is neither universal in time nor in space; as coding fashions change, problems that were once minor can become major). You may prefer to use a language with a different design philosophy, but I think that philosophy is certainly reasonable. Again, without any kind of empirical data, I don't see how this can be settled by anything other than personal aesthetic preference.

> HKT has one of the strongest cases in terms of power-to-weight: it's a very cautious extension of the type system that doesn't really make the language any more complex, since it just means permitting type parameters to be used in ways that concrete types are already allowed to be used.

Maybe, and maybe Java and Kotlin should get HKT one day. But I don't think this feature would be the most important one to add right now, and I can certainly see strong arguments against encouraging higher-order abstractions in general. For one, I find that abstractions-in-the-small take precious mental resources away from far more important things. For another (although related), I think they encourage abstract code of the kind that was common in Java frameworks like Spring, which took Java a long time to discourage in favor of simpler, more concrete code, YAGNI etc.

> Threads, loops and exceptions are notorious sources of bugs and incomprehensible code.

OK, but I strongly disagree (BTW, by "threads" I'm not implying any kind of communication mechanism, like shared memory; Erlang is also based on threads. I just mean one or more sequential instruction stream that can block).

Re:Kotlin: A Language with a Bright Future by lmm on Monday December 04, 2017 @11:58AM (#15845329)
> For another (although related), I think they encourage abstract code of the kind that was common in Java frameworks like Spring, which took Java a long time to discourage in favor of simpler, more concrete code, YAGNI etc.

I see the fact that Spring was immensely popular in Java for a while as demonstrating just the opposite: that overgeneralisation and second-system effect happen to everyone, even in a language whose design philosophy was oriented towards avoiding it. I see Java's adoption of generics and lambdas as acknowledgement that omitting those features didn't help encourage simpler code, it just made complex code even worse. I think it's the same for HKT and similar abstraction tools.

Re:Kotlin: A Language with a Bright Future by pron on Monday December 04, 2017 @12:06PM (#15845409)
Like I said -- maybe, and, indeed coding-style fashions change. Something that wasn't important ten years ago may be important today. Java/Kotlin try to follow the mainstream, not break new ground. It's good to have such languages (I, personally, prefer them), just as it's good to have more adventurous ones. Java explicitly aims for a last-mover advantage, not a first-mover advantage. The goal is to learn 1, what works, and 2/ what's really important from other languages, and only then, maybe, adopt the most useful and important features.