3 ms·

Its not the same at all - for one, in Java null can be assigned to any type. There is a difference between the inability to prove certain things and having gian

by spion 11y ago

Its not the same at all - for one, in Java null can be assigned to any type. There is a difference between the inability to prove certain things and having giant holes in the type systems that nullify most guarantees. Additionally, I believe that the effort required to write Haskell code is vastly over-estimated. Its not harder than other languages - just different enough that a lot of knowledge doesn't transfer.

pron 11y ago
> Additionally, I believe that the effort required to write Haskell code is vastly over-estimated. Perhaps, but so is the ability of Haskell to produce more correct program more cheaply. The Haskell type system is really not powerful enough to verify even the basic monad properties, let alone a simple sorting algorithm. OTOH, you can eliminate null-pointer errors with much simpler type type systems than Haskell's (e.g. Kotlin's). Haskell's type system exists at one point on a spectrum, Java's at another and Kotlin at yet another (but close to Java). It has not been shown which point results in less total development cost, nor that there aren't any other points with better results. Also, none of those was contrasted with a hybrid approach that has proven useful at Amazon (write code in Java, verify in TLA+). > for one, in Java null can be assigned to any type. Not with Java 8's pluggable type systems (which are quite advanced, BTW): http://types.cs.washington.edu/checker-framework/current/checker-framework-manual.html http://types.cs.washington.edu/checker-framework/current/che... > There is a difference between the inability to prove certain things and having giant holes in the type systems that nullify most guarantees. I don't know if the distinction is so clear. Type systems aren't axiomatically "good". They exist to serve a purpose, and they come at a cost. Both purpose and costs are points on a scale, so one cannot simply make the general statement that a "sound type system is better than an unsound type system". All you can say about it is that it's sound. Whether it's "better" or not requires some empirical study.
- spion 11y ago
  The distinction isn't too hard to make: a type system's "goodness" is: * proportional to the number of constraints you can express with it (that you're interested in) * inversely proportional the effort necessary to express those constraints * inversely proportional to the number of lies it tells (times probability to encounter a lie) I'd like to expand on #3 via examples: Assignable nulls is an example of a type system lying. It lowers the guarantees without reducing the burden. The more you rely on that lie being the truth in your code, the less useful the type system is in preventing bugs in your code. `null` is a pervasive hole as every time you invoke a method on any object, you may actually be throwing a null pointer exception Checking for null every time will help - now we have the guarantee back. However then we get to another hole which is caused by shared mutable state: if you check for nulls by the time you get to executing the method inside the block the reference may become null. Luckily, this doesn't pertain to code that doesn't deal with shared mutable state, so this "unsoundness" is less "bad" i.e. more avoidable than the previous one. However in the presence of concurrency, immutability or the inability to share mutable state become another useful constraint. So its simply a question of how much potential certain lie has to cause problems in your particular code or domain. For example, the answer for `null` is pretty much "most code". The answer for "bivariant function types in TypeScript" is "a lot less, but here are cases X Y and Z and they are common in our code, and here is how to avoid it.." But yes, I agree that its not a binary unsound vs sound. And I do prefer type systems where I can say "trust me, this results with the type I say it will" when its not possible to express it otherwise. I'm okay with lying to the type system: just not okay with it lying to me.

by spion 11y ago

pron 11y ago

> Additionally, I believe that the effort required to write Haskell code is vastly over-estimated. Perhaps, but so is the ability of Haskell to produce more correct program more cheaply. The Haskell type system is really not powerful enough to verify even the basic monad properties, let alone a simple sorting algorithm. OTOH, you can eliminate null-pointer errors with much simpler type type systems than Haskell's (e.g. Kotlin's). Haskell's type system exists at one point on a spectrum, Java's at another and Kotlin at yet another (but close to Java). It has not been shown which point results in less total development cost, nor that there aren't any other points with better results. Also, none of those was contrasted with a hybrid approach that has proven useful at Amazon (write code in Java, verify in TLA+). > for one, in Java null can be assigned to any type. Not with Java 8's pluggable type systems (which are quite advanced, BTW): http://types.cs.washington.edu/checker-framework/current/checker-framework-manual.html http://types.cs.washington.edu/checker-framework/current/che... > There is a difference between the inability to prove certain things and having giant holes in the type systems that nullify most guarantees. I don't know if the distinction is so clear. Type systems aren't axiomatically "good". They exist to serve a purpose, and they come at a cost. Both purpose and costs are points on a scale, so one cannot simply make the general statement that a "sound type system is better than an unsound type system". All you can say about it is that it's sound. Whether it's "better" or not requires some empirical study.

spion 11y ago
The distinction isn't too hard to make: a type system's "goodness" is: * proportional to the number of constraints you can express with it (that you're interested in) * inversely proportional the effort necessary to express those constraints * inversely proportional to the number of lies it tells (times probability to encounter a lie) I'd like to expand on #3 via examples: Assignable nulls is an example of a type system lying. It lowers the guarantees without reducing the burden. The more you rely on that lie being the truth in your code, the less useful the type system is in preventing bugs in your code. `null` is a pervasive hole as every time you invoke a method on any object, you may actually be throwing a null pointer exception Checking for null every time will help - now we have the guarantee back. However then we get to another hole which is caused by shared mutable state: if you check for nulls by the time you get to executing the method inside the block the reference may become null. Luckily, this doesn't pertain to code that doesn't deal with shared mutable state, so this "unsoundness" is less "bad" i.e. more avoidable than the previous one. However in the presence of concurrency, immutability or the inability to share mutable state become another useful constraint. So its simply a question of how much potential certain lie has to cause problems in your particular code or domain. For example, the answer for `null` is pretty much "most code". The answer for "bivariant function types in TypeScript" is "a lot less, but here are cases X Y and Z and they are common in our code, and here is how to avoid it.." But yes, I agree that its not a binary unsound vs sound. And I do prefer type systems where I can say "trust me, this results with the type I say it will" when its not possible to express it otherwise. I'm okay with lying to the type system: just not okay with it lying to me.