1. Call-by-value gives us both the ability reason by induction. It also typically results in the presence of non-pointed types, whereas Haskell only has pointed types.
2. Call-by-value gives us the ability to safely interleave effects. Now, I know you all think we should not be doing that at all, but I would say that this is only true in some cases. The point of reifying an effect in a monad is not because "effects are icky"; it is because we have written a non-extensional operation using effects, and we want it to be an extensional function. Wrapping it up in the monad "completes" the operation as such. However, there are plenty of extensional functions which may be written using computational effects (such as memoization): these should not be wrapped up in the monad. (FYI, it's the effects that preserve extensionality which is what Bob calls "benign effects", to the consternation of Haskell developers everywhere.) ML gives us the fine-grainedness to make these choices, at the cost of some reasoning facilities: more proofs must be done on paper, or in an external logical framework. I tend to think that the latter is inevitable, but some disagree.
I am hoping for a middle-ground then: something like ML, in that effects are fundamental and not just bolted onto the language with a stack of monads; something like Haskell, where we can tell what effects are being used by a piece of code.
The story hasn't been fully written on this, but I think that Call-by-push-value can help us with both recovering the benefits of laziness as well as reasoning about effects.
3. Modularity is something which Haskell people simply do not take seriously, even with the new "backpack" package-level module system they are building. One of the most-loved reasoning facilities present in Haskell depends, believe it or not, on global scope, and is therefore inherently anti-modular (this is the uniqueness of type class instances). As a result, you can never add modularity to Haskell, but we may be able to back-port some of the more beloved aspects of Haskell to a new nephew in the ML family.
(Confusingly, laziness advocates often say that their brand of functional programming has better "modularity" than strict, because of the way that you can compose lazy algorithms to get more lazy algorithms that don't totally blow up in complexity. I would say that lazy languages are more "compositional", not more "modular"—I prefer to use the latter term for modularity at the level of architecture and systems design, not algorithms.)
> I think that Call-by-push-value can help us with both recovering the benefits of laziness as well as reasoning about effects.
I would be very interested to hear why you think that, or just have some links on the subject. In particular it's not clear to me how CBPV helps us reason about effects.
Could you expand on effects which preserve extensionality some more? I'm fairly sure I understand it, but I've never quite follows what Harper's "benign effects" meant in detail and I'd like to see how it all connects.
So extensionally equal simply means that there is a model with and without the effect such that extensionally, according to some model of observation, we cannot discern the existence of the effect?
I wasn't thinking about models, but perhaps you could? I just mean that you get the same results for equal inputs; laziness is fine in this respect (but not in the presence of some other effects).
The best argument for John's thesis is the proliferation of ML derivatives in industry: Swift, Rust and Facebook's Hack. I'm really looking to Facebook's Flow which adds an ML style type system to Javascript.
I would be very cautious about saying "popularity" or "proliferation" suggest that something is good. The ML family happens to have proliferated very nicely, but this is not why it is good.
> Modularity is something which Haskell people simply do not take seriously
Plus, the build/module/packaging/dependency resolution story, even when doing all the recommended best practices involving sandboxing Cabal and leveraging Nix are just plain embarrassing.
There are so many smart Haskell people. I don't understand how any of them could consider this clusterf*ck to be remotely acceptable.
In Haskell, sandboxes usually force you to rebuild stuff which you have already built over and over.
Anyway, sandboxes are pointless hacks which wouldn't be necessary if things had been done properly from the beginning.
They are like Node.JS ... yes, it enables you to develop with JavaScript on the server, but how the hell did you end up with using JavaScript in the first place?!
Sandboxes aren't pointless hacks which shouldn't be necessary. It's a lot more difficult for static languages to get right, and solutions like Maven have had tons of work put into them.
You say "if things had been done properly from the beginning" implying you know some mistakes that were made. What mistakes were made in the beginning?
Do you have any ideas how the problems cabal has could have been avoided? There are very intelligent people working on this problem and it is well known that dependency resolution isn't an easy problem.
> solutions like Maven have had tons of work put into them
Maven required tons of work because it's written in Java, not because the ideas behind it are advanced in any sense.
It's sounds absurd because it's so simple, but the issue is that Cabal/GHC doesn't deal with versioning. Different versions of the same library are not properly treated as different artifacts. That's why everything breaks if you install it into a global namespace.
"Great, let's just multiply our namespaces!" is the obvious knee-jerk reaction, but not a great solution.
> There are very intelligent people working on this problem
That sounds great! Because until now I have mostly seen "very intelligent people" who have been busily in denial that a problem even exists.
2. Call-by-value gives us the ability to safely interleave effects. Now, I know you all think we should not be doing that at all, but I would say that this is only true in some cases. The point of reifying an effect in a monad is not because "effects are icky"; it is because we have written a non-extensional operation using effects, and we want it to be an extensional function. Wrapping it up in the monad "completes" the operation as such. However, there are plenty of extensional functions which may be written using computational effects (such as memoization): these should not be wrapped up in the monad. (FYI, it's the effects that preserve extensionality which is what Bob calls "benign effects", to the consternation of Haskell developers everywhere.) ML gives us the fine-grainedness to make these choices, at the cost of some reasoning facilities: more proofs must be done on paper, or in an external logical framework. I tend to think that the latter is inevitable, but some disagree.
I am hoping for a middle-ground then: something like ML, in that effects are fundamental and not just bolted onto the language with a stack of monads; something like Haskell, where we can tell what effects are being used by a piece of code.
The story hasn't been fully written on this, but I think that Call-by-push-value can help us with both recovering the benefits of laziness as well as reasoning about effects.
3. Modularity is something which Haskell people simply do not take seriously, even with the new "backpack" package-level module system they are building. One of the most-loved reasoning facilities present in Haskell depends, believe it or not, on global scope, and is therefore inherently anti-modular (this is the uniqueness of type class instances). As a result, you can never add modularity to Haskell, but we may be able to back-port some of the more beloved aspects of Haskell to a new nephew in the ML family.
(Confusingly, laziness advocates often say that their brand of functional programming has better "modularity" than strict, because of the way that you can compose lazy algorithms to get more lazy algorithms that don't totally blow up in complexity. I would say that lazy languages are more "compositional", not more "modular"—I prefer to use the latter term for modularity at the level of architecture and systems design, not algorithms.)