6 ms·

While the solution described is cool, it only applies to problems that can be solved with union types in F#. That's cool, but things get much more complicated

While the solution described is cool, it only applies to problems that can be solved with union types in F#. That's cool, but things get much more complicated when trying to describe the concept of a non-empty list (still possible, but I don't believe is included in F#'s library), or near impossible when trying to describe things like a number within a certain range, or various relationships between the arguments of a function or of a type. I mean, when you're constructing something like "Segment(x, y)" (or "Segment of double * double" in F#, not sure if I got the syntax right), how do you express that the X coordinate needs to be lower than the Y coordinate? And then the biggest modern challenge is to model state machines for asynchronous communications, which implies working in the presence of non-determinism. Good luck modeling that with a static type system. Basically there are things that can be expressed in a statically typed way, by means of a good enough type-system, but there are always invariants that can only be checked at runtime. Hence assertions sprinkled in the code are still valuable even in a language like F#, because if you're going to fail, it's better to fail as fast as possible.

josteink 11y ago
> And then the biggest modern challenge is to model state machines for asynchronous communications, which implies working in the presence of non-determinism. Good luck modeling that with a static type system. I don't think async really matters at type-level. What matters is the failure-mode. And Haskell seems to be doing this just fine, by abstracting IO into its own aspect which can either succeed or fail, and thus separates the domain-model from the failure-modes. It's by no means impossible, and it's pretty defeatist to assume we all have to end up in some sort of dynamic non-typed nodejs-like blob as soon as you invoke Async or network operations. Even C# handles this quite well, and fully typed all the way.
- bad_user 11y ago
  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).
wereHamster 11y ago
Can't comment on F#, but in Haskell you'd create a special datatype and use smart constructor which only allows to create a value which conforms the requirements: data Segment = Segment Double Double mkSegment :: Double -> Double -> Maybe Segment mkSegment x y | x < y = Just (Segment x y) | otherwise = Nothing There are things you can check at compile time, and for that F# and other strongly typed languages are great. And if that's impossible they can still force you to do these checks at runtime. And with such great support for custom types, you can rely on complex invariants in large parts of your application. In the example above, if you have a `Segment`, you know that x < y, even if the compiler can't prove it.
- pron 11y ago
  That's still a runtime check rather than a compile-time guarantee, and whatever the type does guarantee (i.e. constructed instances are OK) is identical to throwing an exception (or a checked exception if you want to guarantee handling) in an OO constructor.
  - the_af 11y ago
    But it's not identical to throwing an exception, that's the thing. The signature immediately makes it explicit you must deal with the possibility of failure; it's encoded in the type. You cannot "forget" to handle it the way you can forget to catch an exception. The closest to this are checked exceptions, which turned out to be a bad idea and most languages I'm aware of don't have them (and the consensus in the case of Java is that they were a mistake).
    - pron 11y ago
      > The closest to this are checked exceptions, which turned out to be a bad idea But that's because lots of people actually used them and came to the conclusion that they didn't want to manually handle every exceptional case at the call-site. People realized that if an operation has two outcomes, but one of them would cause the entire computation to fail and that outcome happened only 1/1000 of cases, they'd rather just ignore it, and catch any exception up the stack. If many people used Either/Maybe they might come to the same conclusion. So we don't know today if Either/Maybe work well just as we didn't know in 1995 if checked exceptions work well -- simply because the pattern hasn't seen enough use yet (and I have no reason to believe that the conclusion would be any different, namely that a possible though unlikely outcome might want to be handled collectively not near the call-site).
pron 11y ago
> While the solution described is cool, it only applies to problems that can be solved with union types in F#. I'm not even sure it achieves that. Without linear types (or "typestate"), if an operation (say, delete) actually modifies a database or a file -- as would normally be the case -- you can have outdated references of the wrong type (ActiveUser) pointing to the same DB record. They've just introduced a far worse runtime inconsistency (while staying perfectly type-safe)!

josteink 11y ago

> And then the biggest modern challenge is to model state machines for asynchronous communications, which implies working in the presence of non-determinism. Good luck modeling that with a static type system. I don't think async really matters at type-level. What matters is the failure-mode. And Haskell seems to be doing this just fine, by abstracting IO into its own aspect which can either succeed or fail, and thus separates the domain-model from the failure-modes. It's by no means impossible, and it's pretty defeatist to assume we all have to end up in some sort of dynamic non-typed nodejs-like blob as soon as you invoke Async or network operations. Even C# handles this quite well, and fully typed all the way.

bad_user 11y ago
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).

wereHamster 11y ago

Can't comment on F#, but in Haskell you'd create a special datatype and use smart constructor which only allows to create a value which conforms the requirements: data Segment = Segment Double Double mkSegment :: Double -> Double -> Maybe Segment mkSegment x y | x < y = Just (Segment x y) | otherwise = Nothing There are things you can check at compile time, and for that F# and other strongly typed languages are great. And if that's impossible they can still force you to do these checks at runtime. And with such great support for custom types, you can rely on complex invariants in large parts of your application. In the example above, if you have a `Segment`, you know that x < y, even if the compiler can't prove it.

pron 11y ago
That's still a runtime check rather than a compile-time guarantee, and whatever the type does guarantee (i.e. constructed instances are OK) is identical to throwing an exception (or a checked exception if you want to guarantee handling) in an OO constructor.
- the_af 11y ago
  But it's not identical to throwing an exception, that's the thing. The signature immediately makes it explicit you must deal with the possibility of failure; it's encoded in the type. You cannot "forget" to handle it the way you can forget to catch an exception. The closest to this are checked exceptions, which turned out to be a bad idea and most languages I'm aware of don't have them (and the consensus in the case of Java is that they were a mistake).
  - pron 11y ago
    > The closest to this are checked exceptions, which turned out to be a bad idea But that's because lots of people actually used them and came to the conclusion that they didn't want to manually handle every exceptional case at the call-site. People realized that if an operation has two outcomes, but one of them would cause the entire computation to fail and that outcome happened only 1/1000 of cases, they'd rather just ignore it, and catch any exception up the stack. If many people used Either/Maybe they might come to the same conclusion. So we don't know today if Either/Maybe work well just as we didn't know in 1995 if checked exceptions work well -- simply because the pattern hasn't seen enough use yet (and I have no reason to believe that the conclusion would be any different, namely that a possible though unlikely outcome might want to be handled collectively not near the call-site).

pron 11y ago

> While the solution described is cool, it only applies to problems that can be solved with union types in F#. I'm not even sure it achieves that. Without linear types (or "typestate"), if an operation (say, delete) actually modifies a database or a file -- as would normally be the case -- you can have outdated references of the wrong type (ActiveUser) pointing to the same DB record. They've just introduced a far worse runtime inconsistency (while staying perfectly type-safe)!