7 ms·

#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 requi

by spion 11y ago

#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]: http://elm-lang.org/docs/records http://elm-lang.org/docs/records

pron 11y ago
> #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.
- spion 11y ago
  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? :)
  - pron 11y ago
    > 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.
    - catnaroek 11y ago
      «Throw an exception» Runtime is too late to find bugs.
      - pron 11y ago
        That's not what I meant. The presence of an exception in the constructor proves that an invalid `Email` instance can't exist in any expression.
        catnaroek 11y ago
        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.
    - 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.

by spion 11y ago

pron 11y ago

> #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.

spion 11y ago
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? :)
- pron 11y ago
  > 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.
  - catnaroek 11y ago
    «Throw an exception» Runtime is too late to find bugs.
    - pron 11y ago
      That's not what I meant. The presence of an exception in the constructor proves that an invalid `Email` instance can't exist in any expression.
      - catnaroek 11y ago
        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.
  - 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.