Tests vs. Types
kevinmahoney.co.uk
kevinmahoney.co.uk
> 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.
> 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.
You're right about the bottom input. I'll add it to the article.
Prelude> head []
*** Exception: Prelude.head: empty listEither way, pure code can throw exceptions in Haskell. Consider division by zero for example.
[1] https://hackage.haskell.org/package/safe-0.3.9/docs/Safe.htm...
Prelude> :t error
error :: [Char] -> a
Prelude> :t undefined
undefined :: t
Prelude> :t assert
assert :: Bool -> a -> a
Prelude Control.Exception> :t throw
throw :: Exception e => e -> a
I wasn't aware of 'throw' and that certainly weakens my argument. You could maybe argue it is an escape hatch in the same vein as unsafePerformIO, but I don't know how it is viewed by the community.
You could argue I'm playing word games here, and I have some sympathy for that argument. What I wanted to get across is checked exceptions ala. Java (although they are too commonly bypassed in that example). Maybe moving it to the documentation section is a good compromise.
Okay, but in the case of GHC you actually can recover from them.
> I wasn't aware of 'throw' and that certainly weakens my argument. You could maybe argue it is an escape hatch in the same vein as unsafePerformIO, but I don't know how it is viewed by the community.
Asynchronous exceptions are pretty widely accepted as the way to interrupt a long-running pure computation. `error` is pretty widely used on identifying programming errors and pretty well reserved to that case. There is some dispute over whether exceptions or Either is more appropriate to dealing with exceptional conditions in IO; more reluctance around exceptions for reporting exceptional conditions outside of IO (partly because of the "only catch in IO" restriction, and substantially because we have other, good methods).
> What I wanted to get across is checked exceptions ala. Java (although they are too commonly bypassed in that example).
I'd like to see some language flesh out checked exceptions with parametric polymorphism. Alack, this is not what Haskell has (yet?) done.
For synchronous exceptions Haskell is sort of middle-of-the-road, differing from other languages mostly in providing other options that are substantially better for many use cases.
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.
For example, with django's forms, you are forced to call validation (`form.is_valid()`) before you can get the result of said validation (`form.cleaned_data`)
So referencing `form.cleaned_data` before `form.is_valid()` is incorrect....
If you had to port something like Django's forms to Haskell, you could instantly get rid of this issue because such behaviour is impossible to express in the language.
In Haskell you would likely write a `validate` function that takes a form, and returns either a validation error or the validated data itself: `let maybeCleanedData = validate form`
The type system that makes effects explicit (really, the immutable nature of everything, but one and the other usually synergise well) means that your API is forced to be a saner one.
You can take what you learn from these type systems and bring it back to Python though. Like you said, most errors are logic errors. But logic errors can often be helped along by dangerous APIs. Types and removal of stateful code can give you the boundaries to rule out many designs that can come back to bite you.
I hear that relatively frequently from people who consider types to be things like functions, strings, integers, and other "representation types". But the benefit of type systems, especially type systems as expressive as Haskell, is that you, many times, can encode your logical invariants in the type system by introducing new nominal types. For example, you can introduce a new type for each type of ID in your system, like CustomerID, ExperimentID, EventID, which prevents you from mixing those up. You can use types to distinguish between mutable and immutable data structures. It's perfectly okay to use object identity when comparing immutable data structures, but it's usually a bug if the data structure is mutable.
When you take a more expansive view of what type systems can offer, they're more useful.
I find the flexibility of the type system to share some similar properties with C++'s more advanced features. Used sparingly they can be quite powerful but come with a complexity that few mortals will be able to comprehend. In a distributed system, for example, you can encode an invariant in the type system that will constrain the execution to only valid states. This is immensely powerful. However you can also model arbitrarily complex computations into the type system which will make sense to no one but the author who wrote it.
One thing I do miss in Python that a type system gives you is the compiler's ability to do exhaustive pattern matching. Forcing you to deal with every case explicitly is a huge advantage. In fact, I'm currently working on a formal specification of eventlet's Semaphore class as an exercise (I'm in the process of learning) as we've found just such a bug in a large Python code base where a particular exception is not caught and locks up the whole system. An exhaustive pattern search would have forced the authors to deal with that exception and this bug wouldn't have surfaced.
I don't understand this statement. The only thing immutability provides here is the ability to know that an object didn't change by knowing that it's the same object. There's no guarantee of value equality from identity unless all objects are interned.
With immutable data structures, you know that x == y implies, even if x was initialized a while ago, that the data is the same. With mutable data, that's not true -- perhaps the values referenced by x have changed value in the meantime, so x == y does not imply that the data is the same.
A richer type system allows you to move more logic into type system.
Every programming language has syntax, not every programming language has static types.
I think you can separate these pretty cleanly.
You can, and probably should, but it's more of an engineering distinction than a theoretical one. Syntax and types are both rules for how phrases can fit together. And sometimes it blurs - I understand that at least one C++ compiler parses with an overly general parser, collecting several results and disambiguating with type information.
> Every programming language has syntax, not every programming language has static types.
Not every programming language has "static syntax" - some allow you to adjust the parser, and some don't do any checking of the whole file (much less the whole program) before they start running the first bits of it.
What is your definition of a type error? The point of more advanced type systems is to allow programmers to express more information about the program in the types so that the compiler can check them and report mistakes. I've done my share of Python coding and many of my errors were definitely type errors (even if they didn't necessarily raise TypeError).
(this is a question I'm genuinely curious about)
In my current project, I am parsing and analyzing a dialect of SQL.
As you say, "we must develop systems with incomplete knowledge". Had it been necessary that I get my rules right up front, there would be tremendous pain - the documentation is inconsistent, incomplete, and incorrect. Tremendous agreement there.
This is no case for foregoing types.
In order to write code we must be defining expectations of how our system works. Even ideally loosely coupled, code depends on the behavior of other code. When we learn that a given interface is no longer going to work, we need to find and change everywhere that relied on that interface.
Working in Haskell I was able to sketch out a preliminary and incomplete set of rules; as I found them not to work I could change them - with tremendous assistance in finding exactly the points that needed to change in tandem. Working in Python earlier this year, much smaller changes to much simpler code has been substantially more painful.
Not my experience either. We commonly hear the refrain "Haskell does not allow you to do exploratory programming". Personally I prefer exploratory programming in Haskell to any other language.
A more ambitious example: imagine the web with JavaScript replaced by Haskell. Your code compiles and typechecks in your browser, but that doesn't guarantee that it will do the same in mine, or a different version of yours, or tomorrow's new browser. So these static type guarantees are very weak because they only apply to a single runtime environment.
The less control you have over the runtime environment, the more important dynamic typechecks become. You can also have static type checking, but you have to be prepared for the fact that your static types will be different at runtime. This property confounds most languages with static type systems, including Haskell.
Wait... What? Are you saying that natural numbers in South America in 1990 century is different from natural numbers in Europe 2010? So how can types be different depending on browsers?
Of course, if the browser implements a "compiler" that doesn't follow the basic principles reported in the standard of the language, it'll happen. If some joker wants to call `Int` a `String`, problems will happen. Otherwise, it is not true.
Languages are getting better at type inference, but things like JSON parsing are more rigid and explicit. It just feels jobbish at times.
Directly related to the typechecker? Non-incremental (cold) compile times.
The most common error I make myself is typos, but those are often (but not always) fixed quickly. The most common mistake I see getting to production is not handling a return value or an exception because it was assumed it couldn't happen.
Types can help with both of these things, and tests less so - because often if you're making an assumption about the return value of a function, it's because you haven't considered the possibility and you don't write a test for it.
A dynamic language can certainly be good enough, but in my opinion never ideal.
Exhaustive case matching is very useful, I agree. It is a common error in Python code (and in a similar fashion, to catch all exceptions however inappropriate).
> A dynamic language can certainly be good enough, but in my opinion never ideal.
If I think about it scientifically there are many cases where Python is ideal.
For example the scientific Python stack, Jupyter, etc is very popular and, "ideal," in the sense that people frequently use it to get real work done. They don't have to categorize every expression and can instead focus on the data and transformations. As a data-exploration tool Python can be said to be ideal.
It seems ideal too as the implementation language of OpenStack where the community supports over 4+ million lines of Python code. Could OpenStack have been better written in Haskell? Maybe. However thousands of contributors seem quite comfortable with Python and the process around developing reliable infrastructure software seems to catch critical errors in practice.
I believe that strongly-typed functional languages are awesome. There are many situations where I'd prefer one over the other. However I don't deal in absolutes and don't believe Haskell is going to be the hammer that screws every dowel.
You'll find plenty of those. So people are wasting time tracking and fixing something that could have been found by a machine (a compiler in this case) in microseconds. A colleague of mine once stated: "unit tests are a poor man's compiler".
The only explanation I can think of is that the type system makes it harder to write incorrect tests by refusing anything that doesn't make sense, from a type point of view.
This can be frustrating, but the only reason it feels easier in a dynamic language is that the compiler lets you get away wih more. It's easier to write incorrect tests. I hardly think this is a good selling point.
That way, not only do you get to write a better test - a whole class of errors is gone, just not possible anymore - you also have a more modular system, the components of which you can test individually.
I think his example of system time is a good one because an abstraction in that case often only serves to enable testing. If testing is already possible, then that abstraction is just unneeded complexity
What I understood was, changing the way time is handled for your entire Ruby process in order to test that some publish function sets the right date is good practice. As opposed to, say, have it expect a date argument, which lets you test it without side effects that can impact absolutely everything else, and gets you a more powerful feature, publishAt rather than just publishNow.
If I understood this correctly (which I honestly doubt), I don't think our conversation serves much purpose. You seem to regard as good practice what I consider utter lunacy. I don't pretend that I'm right, just that there's absolutely no chance that we'll agree on this.
That being said, your point about introducing abstraction for the sole purpose of enabling tests is well made. My experience is that you'll often end up glad you abstracted over whatever it was you needed for the tests and use it in live code, but not 100% of the time.
But if the alternative is global mutable states, I'll consider un-needed abstraction the lesser of two evils and gladly embrace it.
It's a test. It's not production code. It runs and is able to verify behavior. It runs isolated, and no other code is running when it does.
Building publishAt is more powerful than publishNow, but building something more powerful than what you need is hardly good practice. And you still end up with the problem of how you test the code calling publishAt.
This isn't some whack job in the corner saying something he came up with is a good idea. This is how the Ruby community thinks and writes software, with great success. And it does in fact clash with other communities.
The point of this discussion isn't really whether one approach is better than the other. The point is that our tools (specifically dynamic languages with flexible metaprogramming) drastically influence our view of what is acceptable. Your strong disagreement demonstrates the point.
It seems to me that, if you're able to unpack that all and get at why these dramatically contradictory beliefs are held, someone is likely to learn a lot (perhaps both parties!). That sounds like good purpose to me.
Anyway, I agree monkey patching in tests can be pretty convenient! But I personally think it's also a bad idea because it means that your tests are now coupled to the internal implementation of the code under test. That is, if you refactored the implementation, the test could break. Passing testable dependencies explicitly avoids this problem and avoids the need to monkey patch in tests.
I think DHH describes a great example that illustrates a big difference in philosophy around this: http://david.heinemeierhansson.com/2012/dependency-injection...
Type systems focus on making sure you write the code correctly. They help not at all whether you're writing the correct code. In the end, this is on you, the developer, to express correctness in the type system. So the theory goes if you can define the problem correctly in, say, Haskel's type system, (up front, mind you), you may not even need any tests. But most systems are built with incomplete information. You can't know everything ahead of time. Often what is ultimately "correct" is to ship sooner rather than later, learning what is systemically correct as you go along. This is where dynamic languages do well.
You can definitely TDD Haskell, for example, with liberal use of "undefined" or "error". Same with C++: just throw an exception in code paths you haven't "explored" with tests yet.
Also, the notion that because Haskell has a strong type system you don't need tests is a persistent myth. It's nice to have types to prove certain aspects of your program, but you still need a test suite in any significant project.
I think that given a strong type system there exist tests you might otherwise write that you don't need. And I think that is sometimes confused for "given a strong type system, all tests are unnecessary" (which, in my opinion/experience, certainly does not hold), both by some people advocating type systems and by some people reacting to advocacy of type systems.
Again, my experience is that this is precisely where the type checker gives me the most help.
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...
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);
}
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.
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.
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.
Seems a bit of a non-comment.
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 :)
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!
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.
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
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.
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.
So, all kinds of methods of getting some guarantees out of unsafe code that can be paired with safe HLL's like Haskell.