#1 I might be completely wrong, but I think this might be doable in Haskell with a monad that tracks total time + maybe STM would help for the rest of the requirements (for a subset of the problems)
#2 can also be done by writing a custom type for the table row e.g. MyType and a function mkMyType :: columns -> Maybe MyType that never produces a result if the invariants are not satisfied, then updating your data access layer to only allow MyType to be used in insert/update commands. Or is that not sufficient?
#5 is similar to #1 but easier because of the missing deadlock/starvation requirements
Don't know about #3 and #4
edit: What I'd really like in Haskell are Elm style extensible records [1] to replace the glorified product types with auto-generated functions. Everything else seems really great to me
> #1 I might be completely wrong, but I think this might be doable in Haskell with a monad that tracks total time + maybe STM would help for the rest of the requirements (for a subset of the problems)
I don't think you can have a monad that tracks total time at compile time without dependent types (you might be able to do something like what I think you're suggesting with C++ templates, but even that would be rather limited), and STM is neither a verification mechanism nor an artifact of the type system -- it's an algorithm providing a useful abstraction, not unlike a GC (don't get me wrong, it's a great solution in some cases -- Clojure has it, too -- but it's orthogonal to Haskell's other abilities).
> #2 ... then updating your data access layer to only allow...
That's architecture -- not verification -- and no different from saying we'll keep X and Y as private members of a Java class, and only allow modification through a single public method which we mentally "prove" to preserve the invariant.
Obviously, people write software that fulfills similar specifications all the time and those systems work, so we know how to write them (using architecture, care and appropriate algorithms). Formally verifying them is a different story.
You're right. I didn't mean full formal verification, I just meant controlling the amount of code you do need to verify. There will be axioms of course i.e.
given the axiom "mkEmail :: String -> Maybe Email` always produces Nothing when the email is not correct, and given that other Email constructors are not available"
then the `Email` type is guaranteed to contain a valid email address anywhere in the code.
At least that is where the value is for me - the type system freeing me from reasoning about the same preconditions everywhere, over and over again - as well as warning me when I violate them while changing the code. Is that not enough? :)
Enough for what? Proving the correctness of a sorting algorithm, a distributed algorithm or pretty much any algorithm? Or proving that your request scheduling is fair and free from various failures? No, I'm afraid it isn't. :)
Enough for preventing the most expensive bugs? Well, that requires evidence, but I have the feeling that the answer to that is also no.
It's certainly good for many, more modest things, but the guarantees you happened to mention are as easily achievable with much cruder type systems in much more popular and better-supported languages, too (your own example is the same as having the Email class's constructor throw an exception in Java/C++/C# for invalid emails; that would guarantee that all Email instances are valid).
The question is, is the extra type-expressivity afforded by Haskell -- which is richer than cruder type systems but falls short of other, more popular verification approaches -- worth the extra effort? Unfortunately, at this point in time we can only answer this question based on personal preference and anecdotes.
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.
> 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.
> 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.
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.
That's assuming that exceptions show up in type signatures. (Which they do in Java, granted.) And it's still incredibly noisy compared to pattern matching on Options/Eithers or, even better, chaining them Kleisli Option/Either arrows.
#2 can also be done by writing a custom type for the table row e.g. MyType and a function mkMyType :: columns -> Maybe MyType that never produces a result if the invariants are not satisfied, then updating your data access layer to only allow MyType to be used in insert/update commands. Or is that not sufficient?
#5 is similar to #1 but easier because of the missing deadlock/starvation requirements
Don't know about #3 and #4
edit: What I'd really like in Haskell are Elm style extensible records [1] to replace the glorified product types with auto-generated functions. Everything else seems really great to me
[1]: http://elm-lang.org/docs/records