2 ms·

I wasn't referring to the Async/Task in C# / Futures or Promises in other languages. That model is too simplistic and can only be applied to a limited set of pr

I wasn't referring to the Async/Task in C# / Futures or Promises in other languages. That model is too simplistic and can only be applied to a limited set of problems. Much more interesting is to model actors / components that talk with multiple other actors / components concurrently and whose state and consequently the set of messages it can receive or emit is changing over time, depending on the state of the components it communicates with. In Erlang's actor model it's not defeatist to say that the set of all possible messages an actor can receive can be as useful as Any or String in the face of an ever changing context, coupled with the fact that actors can expose different interfaces depending on to whom they talk to. Imagine a component that on one side receives signal readings determining if some physical asset is available or not and on the other side it accepts commands for that asset, but only if the asset is determined to be available. And the commands are numbers in a certain range that also varies over time depending on the signal readings. And as a more recent example of where static typing fails are the transducers from Clojure. Same problem, as in ... modeling of state machines. > And Haskell seems to be doing this just fine, by abstracting IO into its own aspect which can either succeed or fail If you are talking about the I/O monad, I believe that the I/O monad sucks for doing actual I/O, though it's pretty cool for in-memory stuff. This is because it has baked-in the assumption that those operations are synchronous. Ironically it's the same big problem when you look at, say, the common Iterable pattern and compare it with monads. And I'm not up to date with latest developments, but Iteratees also suck. BTW, I'm a big fan of static typing. I remember a time where I had a hard to reproduce bug that I couldn't understand and I fixed it by eliminating the possibility of it happening through the type system, which was sort of a revelation. But as with everything, there are limits in what you can express and I also believe in runtime constructs where it makes sense.

pron 11y ago
I think session types are what you're looking for, but AFAICT they are very limited (they have the expressivity of regular expressions in expressing the sequence of messages expected over the channel -- no more). Personally, I think that for more interesting properties other formal methods, and in particular model checkers, are the way (and they're much, much easier to use than advanced type systems like dependent types and predicate types, which basically require no less than formal proof). The question, then, of using a type system like F#'s (or Haskell's) vs. C#'s (or Java's) becomes a matter of an entirely different set of tradeoffs, because neither can come close to verifying the kind of interesting properties programs need for verification (and model checkers can), and by comparison, one only helps verifying properties that are only marginally more interesting than the other (and that, too, comes at a cost). I think that much of the benefit of languages like F#/OCaml comes from immutability by default rather than from the type system. In fact, even in the example in the article, the very same (not working but nevermind) approach would have been idiomatic in C#/Java if they, too, were immutable by default. But, of course, immutability has its own costs (unless mitigated by linear types, which also don't come free).

pron 11y ago

I think session types are what you're looking for, but AFAICT they are very limited (they have the expressivity of regular expressions in expressing the sequence of messages expected over the channel -- no more). Personally, I think that for more interesting properties other formal methods, and in particular model checkers, are the way (and they're much, much easier to use than advanced type systems like dependent types and predicate types, which basically require no less than formal proof). The question, then, of using a type system like F#'s (or Haskell's) vs. C#'s (or Java's) becomes a matter of an entirely different set of tradeoffs, because neither can come close to verifying the kind of interesting properties programs need for verification (and model checkers can), and by comparison, one only helps verifying properties that are only marginally more interesting than the other (and that, too, comes at a cost). I think that much of the benefit of languages like F#/OCaml comes from immutability by default rather than from the type system. In fact, even in the example in the article, the very same (not working but nevermind) approach would have been idiomatic in C#/Java if they, too, were immutable by default. But, of course, immutability has its own costs (unless mitigated by linear types, which also don't come free).