8 ms·
Tests vs. Types
- tumdum_ 11y agounsafePerformIO invalidates any guarantees in Haskell :(
- dllthomas 11y agoLess than you might think, in practice. I see unsafePerformIO used three places. First, debugging. While there are sometimes better approaches, this is unobjectionable. Second, I'll sometimes use it in throw-away scripts. Here I am knowingly losing some guarantees, but in a sufficiently constrained portion of the system that it's rarely a problem. Third, where it's known to be safe and necessary. This one is the most worrisome, but the community is pretty at expecting uses to 1) be very rare, and 2) have both safety and necessity justified. Really, the fact that all values are inhabited by bottom is a bigger issue. Still, IME, Haskell provides guarantees that are sufficiently reliable to be tremendously useful.
- 15155 11y ago> where it's known to be safe and necessary To give a valid, non-objectionable example: FFI that is known to be pure will often be wrapped with unsafePerformIO to present a clean interface to Haskell code.
- chadaustin 11y agoIndeed. Consider https://github.com/chadaustin/buffer-builder/blob/master/src/Data/BufferBuilder.hs#L164 https://github.com/chadaustin/buffer-builder/blob/master/src... The API is pure, but it's implemented with a high-performance effectful monad, and none of the implementation details are exported. A perfect use of unsafe[Dupable]PerformIO.
- tumdum_ 11y agoI think you misunderstood me. I'm not saying it is common to use unsafe functions in Haskell for 'bad things'. All I'm saying is that due to existence unsafe functions it is possible to lie about your real side effects and memory safety. Which considering that op article was about guarantees seems to be critical issue. If I give you only the signature of function, You can't be sure what exactly it's doing, just like in C - http://lpaste.net/5209148331879563264 http://lpaste.net/5209148331879563264
- kpmah 11y agoI deliberately ignore that :) I don't think escape hatches added as a practical concern should count against the language, as long as they're used appropriately by the community. You can defeat Rust's guarantees by using an `unsafe` block, and you can defeat Python's memory safety by adding a C extension. Like I say at the start, if I were going to be strict about this it would be a very short blog post!
- nickpsecurity 11y agoThere's methods for handling that safely even down to assembler language or gates. Quite a few. FLINT was first I saw. There's also SPARK with integrity checks that assume hardware or something else might goof. Chlipala's Bedrock can emulate some of it. Microsoft came up with one, Vx86, for their VCC verification system that they applied to Hyper-V. They also did CoqASM and used TAL in VerveOS. So, all kinds of methods of getting some guarantees out of unsafe code that can be paired with safe HLL's like Haskell.
- dllthomas 11y ago> With dependent types, the line between tests and types becomes blurrier. I came to the same realization a while back. In principle, in a sufficiently expressive system one could encode any unit test as a type - although whether that could ever be useful is a separate question...
- adamnemecek 11y agoThis way one of my takeaways from Curry Howard isomorphism.
- js8 11y agoExactly. Well, mathematicians do that, they encode everything in the type, which they call the theorem or lemma (while the program itself is the proof). But mathematicians, it seems to me, tend to do a lot of proof copy-pasting, unless they use category theory or something like that.
- dllthomas 11y agoSome nits to pick, on the Haskell: > No exceptions > > Exceptions are also a side effect handled by the type > system. We know our function is pure and won’t throw > an exception. This isn't the case for Haskell. > The input can either be true or false. Once you have > tested the result of these two possibilities, you > have the holy grail. No exceptions, no infinite > loops, no incorrect results, no errors. Almost. The input can also be bottom (a thunk that, when forced, loops infinitely or raises an exception). In that case, if the function tries to inspect the input then the function will also be a thunk that, when forced, loops infinitely or throws an exception. If the function does not inspect its input, it may still return a value (e.g. `const True`).
- kpmah 11y agoCould you expand on your issue with exceptions? In this article I'm using the distinction between exceptions and errors from https://wiki.haskell.org/Error_vs._Exception https://wiki.haskell.org/Error_vs._Exception You're right about the bottom input. I'll add it to the article.
- tazjin 11y agoPure code can (unfortunately) throw exceptions, e.g.: Prelude> head [] *** Exception: Prelude.head: empty list
- agentultra 11y agoWhat this article ignores is that in practice one must read the source code to understand the function. You can be reasonably certain that the Python function doesn't harm your grandmother that way. I understand that strong functional programming is going to catch type errors at compile time and force constraints on the values in your program but it's quite rare that I've encountered a type error in a Python program. What I most often encounter are logic errors. We don't write formal specifications for safety-critical code often enough. Your program will still have errors of this kind if you don't think clearly enough before you start writing code. There are nice things strong, static typing of the functional variety offers certainly -- but it's not a hammer that is particularly useful at cutting boards. There are plenty of cases where a dynamic type system is good enough or even ideal.
- mej10 11y agoWith languages like Haskell you can lift many types of logic errors into the realm of type errors.
- cle 11y agoAt what cost? What are the tradeoffs? (this is a question I'm genuinely curious about)
- 15155 11y ago> At what cost? Directly related to the typechecker? Non-incremental (cold) compile times.
- nickbauman 11y agoDefining those types and the rules of their interaction with a greater type system is also cognitive load you must do up front. In most cases, we must develop systems with incomplete knowledge and must show some progress before all the rules are defined. So you will be changing a lot more code as you learn more than you would in a dynamically typed system.
- fiatjaf 11y agoThis is just Idris propaganda.
- abstractbeliefs 11y agoSo what if it is, if Idris is a useful tool for the task? Seems a bit of a non-comment.
- fiatjaf 11y agoNot at problem at all. I am even looking at Idris right now and I haven't never heard of it before.
- js8 11y agoMaybe that's where the things in programming are going? I think eventually we (programmers) end up with some hybrid system, where lot of stuff that's normally done by hand (refactoring, data transformations, dependency injection, data structure choice, optimization for speed and memory usage, parallelization, deduplication, unit testing) will be done by some theorem prover, working alongside the programmer.
- incepted 11y ago> Maybe that's where the things in programming are going? Doubtful. Idris is probably the most visible current effort in that direction and even it is extremely obscure and barely known beyond the Haskell afficionado circles. And for good reasons: even today, Idris can barely express any program more complicated than the simplest mathematical formulas. Developers need languages that help them express network requests and database queries safely and efficiently, and Idris (and dependent languages in general) are not remotely close to being able to express that.
- kpmah 11y ago(author here) I don't even use Idris! I learnt it a couple of days ago for the purpose of this article. If Idris looks good it's not my fault :)
- 11y ago
- pron 11y ago> If you’re writing software for Boeing or for an iron lung, you may want to consider writing proofs. If you're writing software for Boeing for an iron lung, you may already be using one of a few fully verifiable languages (like SCADE, Esterel) that don't even require proofs -- just a specification -- and have been in common use in safety-critical systems since the eighties. Dependent types are interesting, but they're not widely used simply because there are much more efficient ways of proving safety-critical systems 100% correct. > using a modern type system will give you the most information and guarantees for the least amount of effort I can agree with that one, but I don't agree with the implication that Haskell's type system (or ML's) is the right one for this purpose of giving the most information for the least effort.
- MichaelBurge 11y agoI find that QuickCheck-style tests that randomly choose inputs can have value approaching that of a proof. Code that's even heavily tested with test cases tends to have minor bugs and inconsistencies that need resolving before a proof will work. Code that passes a test with random inputs generally goes through as-is(or with minor restructuring to make the proof easier).
- dllthomas 11y agoI understand the C bit to be mostly an aside, and I wouldn't really say anything there is incorrect, but I think it's worth noting here: In C, `typedef` only "defines a type" as far as the parser is concerned. Beyond that it is treated exactly the same as if you'd spelled it out. A `typedef` can be useful for brevity, for documentation, and to DRY up usage of the type, but it does not get you nominal typing! That said, you can get nominal typing (for a fairly low, but present, syntactic cost) by wrapping primitives in a single-element struct. This keeps the types distinct through the type checker, but is typically stripped away long before code generation so there shouldn't be any run-time cost for the additional safety. As I've practiced, it looks like this: typedef struct price { int64_t v; } price; typedef struct bid { price v; } bid; typedef struct ask { price v; } ask; price price_difference(price p1, price p2) { price r = { p1.v - p2.v } return r; } price compute_spread(bid b, ask a) { return price_difference(a.v, b.v); } Examples, of course, overly simplified for the sake of being examples. If all the .v's are getting messy, I don't feel too bad about unwrapping locally - but passing primitives between functions has become a bit of a smell.