1) It is certainly true, and I've had the experience many times, that "if it compiles, it's correct" applies frequently to Haskell. Even better, I've frequently written code for the first time, hit the compile button, and had it work first time - something that almost never happens to me with Java or C.
2) The huge, HUGE caveat to that is that it's only true for pure and sufficiently polymorphic code. If you're writing anything in the IO monad, or if you're using specific data types (e.g. Int, ) rather than writing polymorphic code, then all bets are off.
There's only one way (ignoring ⊥) to write the forward pipe operator (|>) :: a -> (a -> b) -> b in Haskell. If your code compiles, it's guaranteed to be correct.
There are many, many ways to write the isPrime :: Integer -> Bool function, which differ widely in correctness, understandability and efficiency. Once you move from type variables to concrete types, you open yourself up to many more potential errors.
There are even more ways to write the function deleteFile :: FilePath -> IO (), including but not limited to (i) deleting the file and doing nothing else, (ii) deleting the file and its containing folder, and (iii) wiping your entire filesystem. All of these would type check. Sure, you probably wouldn't make these mistakes, but the point is that the type system won't help you here any more than it would in <insert untyped language here>.
I think Haskell is an incredible language. It's certainly the language I have the most fun with, and I find its approach to parallelism, concurrency, I/O and state to be natural and appealing. But there's a real danger of overstating what Haskell is capable of, and turning off newcomers to the language in the process.
The point of the OP was discussing the safety that can be achieved from pure code.
However, aside from a few libraries and a smattering of very heavily theoretical work, no code satisfies both of those predicates. If you want to write a 'real world' application in Haskell, you're going to have to get your hands dirty with IO and with concrete types, which means that the ability of the type system to prevent you from shooting yourself in the foot is severely curtailed.
The type system is definitely a big part of this, but almost as important are algebraic data types and compiler checks for exhaustivity when scrutinising values of such types.
Maybe I've only worked with amazing super hero developers (not likely), but the type of bugs avoided by Haskell's type system just aren't a big problem in any of the projects I've ever worked on.
The difficult bugs are almost always mistakes in the requirements and design errors, which become even more difficult to fix when you have a bunch of code.
On the other hand, I guess I could see type errors being a problem if you often write hundreds of lines of code before trying to compile and run it...
Those are certainly the biggest problems in building software, but not the types of problems this particular article is talking about overcoming.
(I think we're both in agreement on this)
For example, the type system can differentiate mutable code from immutable code. This means you will never get a mutable data structure when you don't expect it. I've seen several rather subtle and hard-to-catch bugs in some Python code I used to work with because lists were being mutated in the wrong place.
Haskell also makes it much easier to create lightweight new types (with the appropriately named newtype keyword :)). This means that there is no reason not to create different types for semantically different numbers--you can tag all your specialized numbers with a special type. Now, other languages let you do this as well, but in Haskell there is neither a runtime nor a syntactic overhead: numeric literals still work (they're polymorphic), standard numeric functions still work and the runtime representation remains exactly the same. But it will ensure your functions always get the right sort of number. As a practical example, you could differentiate between px and em for CSS measurements (I'm not sure if any library does this, but it is possible).
The type system also makes sure that you cover all the possible cases when you consume (e.g. pattern match on) some data type. I've certainly had bugs crop up when I forget some weird edge-case. Haskell warns about this possibility at compile time.
For constraints that cannot easily be expressed in the type system, there is a pattern called a "smart constructor". This is basically a wrapper function that verifies your invariant; any function that depends on it will force you to have used this function. This way, if the invariant is violated, the code fails immediately clearly. This also makes sure that anybody using those functions actually considered the invariant.
There are a bunch of other uses I haven't listed. For a web development example, I believe that Yesod uses the type system to ensure that all your internal links point to valid locations in your web app.
This is not a an exhaustive list in the least. The important point is that the Haskell type system can do quite a bit more than that of more popular statically typed languages like Java or C#, and, just as critically, makes using these more extensive features easier. There is much less overhead to creating a new type in Haskell than there is in Java, which makes it more likely that programmers will use them more extensively.
Now, of course no type system can possibly protect you from design or specification problems. However, there are still a whole bunch of subtle bugs that can sneak into your code but would have been caught by Haskell's type system. Most of them would probably also be caught by a good test suite, but the type system gives you most of them effectively for free. This also makes writing tests simpler because you do not have to test anything proved by the type system.
If an identity function is too simple, consider "compose :: (a -> b) -> (c -> a) -> (c -> b)". I think it can be proven that if you write an implementation that passes the type checker for this signature, the implementation is necessarily correct.
I can write:
id :: a -> a
id = id
val id : 'a -> 'a
fun id x = id x
id x = id x
id :: a -> a
id a = case (a,unsafePerformIO (print "rm -rf *")) of (x,()) -> a
id :: a -> a
id a = case (a,ack 4 3) of
(x,0) -> x
(x,_) -> x
ack 0 n = n+1
ack m 0 = ack (m-1) 1
ack m n = ack (m-1) (ack m (n-1))
What in the hell are you two talking about and why shouldn't I take this as a sign that I should avoid Haskell at all costs?
I was merely pointed out that last part in the most succinct way I knew how.
You should definitely not avoid Haskell at all costs. I would characteristic programming as the process of constructing systems and managing complexity. If you have a greater exposure to languages and paradigms then you have more tools at you disposal for doing your job. A programmer may be able to get by without knowing anything about Haskell or functional programming in general, but that's only because they don't realize when they are kludging something that is so simple if only it was thought about differently.
Thing is, my fellow lispers, and our scheming siblings too, spent most our time talking about programming or actual code. The former being the means or mode to produce the latter.
Why don't Haskellers ever seem to be talking about programming or actual code when I encounter them in the wild?
Haskell seems to be some mad science project that came about after some grad students happened across an ML manual and a bottle of scotch. (At least you guys didn't make that 31-bit integer mistake. Oof, tagged pointers.)
The emphasis on the type system seems to be a bit revisionist to me. The original (pre-Haskell '98) emphasis was on the laziness really. That turned out to be a huge mistake outside of some cute demonstrations for the purpose of understanding the runtime behavior of your code, so you're choosing to ignore this monstrous mistake and instead promulgate this type safety nonsense as if static analysis has gone anywhere in the last few decades.
So back to my original questions, why don't I ever seem to find you people talking about actual code?
When I encounter fellow Python programmers, they're usually talking about cool libraries, solving interesting problems, neat tools they've discovered or made, best practices, etc.
With Haskell it's more like I've bumped into a rather unpleasant evangelical minister or Amway salesman bred with Doc Brown from Back to the Future. It's like the Haskell community has two modes of operation: proselytization and mathematical gibberish.
You're right to say that the field of static analysis has been very active. What you're forgetting is that this has been in no small part due to type theory.
I think the reason you don't find people talking about actual code, as you put it, is because actual code and so called mathematical gibberish are one and the same thing.
Lisp is based on the idea that code are data are equivalent, Haskell is based on the idea that code and mathematical gibberish are equivalent.
I didn't intend to imply that you didn't know the benefits of functional programming. I could have worded that better. Do you know the benefits of typed functional programming?
Having recently delved into lisp, I do miss the static analysis that goes on before the program starts. I realized that I used types to plan out the program before I started coding and I miss having the type-checker picking holes in my plans. I'm determined to stick at it though so that I can see what I'm missing in terms of meta-programming and other dynamic features.
Yes, that's how I know what ML and the tragedies of tagged pointers are.
SBCL supports type annotations, and Racket has a Typed Racket dialect that does type checking insofar as you've provided the types.
Part of the problem that Lispers and Schemers have is that they can add the static analysis to their programs anytime they want through the macro system (hence typed racket). They don't have to hack up the compiler or anything.
The other problem is cultural. Lispers resent implementation-level obligation to a set of rules that were made ignorant of any given problem they may be solving. What if you need to resolve something at runtime? What if you need to resolve something at compile-time? Lisp lets you choose where each should happen.
I feel similarly about purity. I think it makes for a nice default, but I think the degree to which immutability is forced on you in Clojure and Haskell are pretty damned awkward for expressing a variety of problems and not just ones related to IO. It seems especially silly since a lot of code in Common Lisp will by default be pure because it'll just return results based on inputs absent mutation.
Regarding your delvings into Lisp, since you're not unfamiliar with the benefits of functional programming I'd like to recommend a book that will help you break ground with a dynamically typed, multiple-dispatch Lisp with an object system. Get "Art of the Metaobject Protocol". Hopelessly specific to Lisp but glorious nonetheless.
The book doesn't get as deep as I'd like, but it's considered one of the best books on the subject nevertheless.
I must disagree with you on purity though. Purity allows you to apply equational reasoning, it allows compilers to apply optimizations that wouldn't otherwise be possible. It makes multi-threading, if not possible then substantially easier. You do get some of these advantages from having purity by default, but if it's not enforced, you can't get most of them. For me, I see this as an acceptable compromise (actually I don't see it as a compromise at all, if all I got from purity was equational reasoning I'd still use it), but as you point out, the culture amongst lispers is different.
Thanks for the book recommendation, I must admit that I already have a number of books to get through before I'll be able to look into it (including LiSP and "Compiling with continuations"), but I surely will do.
This is how I know about Typed Racket despite not being that keen on Scheme dialects (other than call/cc), I was very excited to see how compile-time typing could work in a Lisp/Scheme.
Consider me shamed, mind sharing a link? I know the quote from Alan Perlis you're talking about, but the Google search results for "perlis languages" is dominated by Fogus's blog post with the same title, and your comment is the first result for "perlis languages c2", followed by a few other wiki pages.
map :: (a -> b) -> [a] -> [b]
And the translation of types to propositions means that the sum type -- either I have () or I have a list, translates to a logical connective of "or". The product type -- I have an a and the rest of the list -- translates to "and" .
The proposition is therefore that, for all a, for all b, if a implies b, then true or (a and list of a) implies true or (b and list of b).
There are several proofs of this proposition, and some of them are useless.
The standard one:
map f  = 
map f (x:xs) = f x : map f xs
There's another one, though:
map f  = 
map f (x:xs) = [f x]
Anyway, this has been a long and roundabout way of saying that, while a good type system give you a lot of nice static properties about a program, you simply cannot ignore dynamic semantics and rely on the types. Well-typed programs are correct in that they will not reach a state where evaluation is undefined / get stuck ("I'm supposed to do what? These are Strings, not Ints!"), but they do not imply correctness of the program, even though they do provide a proof of a proposition!
f :: a -> b
f = undefined
f :: a -> b
f = f
data T a b = C (T a b -> (a -> b))
q :: T a b -> (T a b -> (a -> b))
q (C f) = f
w :: T a b -> (a -> b)
w x = (q x) x
f :: a -> b
f = w (C w)
g :: a -> b
g = (\x -> ((\(C f) -> f) x) x) (C (\x -> ((\(C f) -> f) x) x))
The GADT example no longer seems to work, so changes to GADT type checking might have eliminated it, but the type family one still does.
a :: 'Nothing
a = a
a :: Int#
a = a
fix x = x x
He is not arguing "it works if it compiles" in general. He is arguing "it works if it compiles", because types are so polymorphic. Polymorphic part is actually important. If you don't get that part, you are missing the point.
The libraries he is talking about are for data types, something that the type system (almost by definition) is perfectly adequate for testing. So yes, he's tested it by compiling it. But for any real world Haskell program the type system alone is not enough.
The article never claims you can always use the type system in place of tests. It doesn't even claim that it is a reasonable practice. The only thing it says is that the author did rely on the type system and that he thinks it is reasonable given sufficiently polymorphic types.
In short, you're knocking down a straw man and using it to accuse the entire community of being an arroganet circle-jerk.
The author of the post provided an amusing example of a case where he posits the type system is sufficient and valuable. He didn't claim that the type system would be sufficient for a complete real-world application.
The term "real world" is not meant to slur, it's meant to be accurate. I've shipped code written in Haskell and I deeply understand the huge pain in the arse it is to use in production for applications that are not toys.
Also, how are parsers or in-memory data structures NOT real-world tasks? You never had to parse some bit-stream or stage a sophisticated-enough computation pipeline that required lots of different, intermediate data types?
I'm not sure why you're seemingly dying to make negative blanket statements based on how "it was a pain in the arse" for YOU.
Also, there is certainly plenty of real-world code I would not like to write with Haskell--drivers, for example. However, it seems great for web-apps, which are very "real world" and, naturally, very important on HN.
In my personal experience, it's also surprisingly good for quick command-line scripts in place of Bash or Perl. Writing small scripts for automation and command-line clients for my existing tools was as easy or easier in Haskell than in any other language I've used.
You are implying that computer science is both useless and only consists of implementing toys. What makes your problems "real world" and the problems that haskell is good for not "real world"? What makes something "not a toy"? Parsers and compilers are toys?
If you want to start a discussion about things that make haskell difficult to work with on a daily basis, please do so. Otherwise, kindly stop throwing around insults.
And yet plenty of people (myself included) are using haskell for real world, production, non-toy applications all the time. So either all of us people using it are mentally ill and just imagining up non-existent production haskell code, or your experience reflects your ability, not the language's capabilities.
What is not accurate in that post?
In an ideal world, tests would be subsumed by types, but in reality tests can cover things that types do not.
It would be literally impossible for this to happen in a Turing-complete language, though, because a hypothetical 'perfect' type system would be able to solve the halting problem.
The Haskell 'Bottom' type alludes to this in its documentation, actually: http://www.haskell.org/haskellwiki/Bottom
(Essentially, Bottom is a member of every type, or else the compiler would need to distinguish between a halting program and a non-halting program before accepting the input program).
Now that I've said that, I'll state what should be obvious (and probably is to many/most): failure to compile due to type errors is a big clue I am thinking about something incorrectly or incompletely. It's not like I just twiddle stuff until it compiles. I look at it and say, "Duh! That was dumb of me!" It's like using Unit Analysis working out a long physics problem... errors in your thinking about it are very likely to show up in unit analysis. The chance of you coming up with a bogus equation that passes unit analysis is pretty small. When it doesn't pass, you have a good look and find where you went wrong rather than merely tweak.
Interesting paper along those lines:
"Types for Units of Measure: Theory and Practice":
add :: Integer -> Integer -> Integer
add x y = x * y
This error can be caught if you put units of measure into type system. F# can do this, and addition function will have type int<a> -> int<a> -> int<a> while multiplication int<a> -> int<b> -> int<a * b>; for example, int<m/s> -> int<s> -> int<m> might be a function taking velocity and time, and returing distance. I think Haskell has libraries for this.
Similarily, add x y = x - y would be detected if (-) required a group, while (+) worked for monoids only.
However, it would be rather hard to create a type system detecting a typo in:
quadruple x = 3 * x
It's also a matter of how much polymorphism you have. There are lots of functions `Integer -> Integer`; there is only one total function `a -> a`. (This is the parametricity theorem mentioned by sanxiyn in http://news.ycombinator.com/item?id=4215055 .)
(You could argue that a (correct) transformation that sends space usage way up may actually change even extension equality, in the sense that it could result in the transformed algorithm failing on a given piece of hardware when the original algorithm would have succeeded. However, my understanding is that the state of 'realistic' computer science, where hardware limitations are part of the reasoning, is in a much more primitive state than 'idealised' computer science.)
But complicated code may work with non-opaque types, and so it could still be reliable without tests.
Something that helps in this regard is travis-ci. It's a free CI server and if you have at least some level of testing, you have some level of confidence.
After the code has been tested, he still doesn't know that it works, only that it sometimes produces the expected output. (As a mathematician, it's a lot easier for me to trust a proof than an empirical verification; but I agree that what the HM type system proves is not always what one wants it to prove.)
It's an amusing anecdote. Even when using Haskell, there are some obvious constraints to relying on the compiler as the sole validation of correctness.
In particular, the kinds of errors that still may exist are ones where the implementer has a fundamental misunderstanding of what needs to happen. The code may correctly implement what he wanted it to do, but what he wanted it to do is wrong.
If you still object, consider: I'm describing the scientific method.
As he and others have pointed out, the author was pretty up-front about the scale (relatively small; looks like a few hundred LOC) and nature (implementing an extant, well-defined API) of the problem. It's not an application as you suggest, and the author doesn't suggest it's a good idea for applications, either.
The conclusion isn't "use Haskell & never test your code!". After all, he explicitly offers no conclusion. :) It's just an example of how, sometimes, you can be reasonably certain that your Haskell program is correct when it compiles.
Myself, I'd still run it, or at least QuickCheck it. I don't trust myself not to write logically sound, completely incorrect code.
However, if you prove the right thing, your code is correct. If you test the right thing, you code is correct in the cases you tested.
And yet, for whatever reason, only having tests is fine but only having proof isn't.
Only having tests is "fine" for most circumstances because, unfortunately, proofs are intractable for most systems. During a software engineering talk I recently attended, an interview candidate stated that the largest proved-correct code base is on the order of 10,000 lines of code. Most people don't have the resources to do even that.
But, philosophically, I always want tests for the same reason that I run experiments: I want empirical evidence, not just reasoning. Empirical evidence increases my confidence that we have accounted for what we think we have.
(Not that writing unit tests for haskell code is a bad idea - QuickCheck is WAY more powerful than junits, for example)
Indeed. What I meant was that basically:
P(HaskellCodeCorrect|Compile+QC+UnitTest) =~= P(OtherCodeCorrect|Compile+UnitTest)
If I never ran my code, it wouldn't have any bugs either, no matter what language I was using.
I guess it does help explain all the half-assed packages on Hackage.
nothacker 42 minutes ago | link [dead]
I have some open source projects that I've released on multiple occasions without having tested them. I think people make the assumption that things that have adequate documentation and comments/support tickets, etc. that indicate use, that they are tested before release. That is simply untrue. You get what you get. That is true in the world of both paid and unpaid open-source and closed-source software and well as life in-general.
I'm not criticising, just curious and in the pub.
late 14c., obs. verb replaced by conjecture (v.). Also in form congette.
At first TDD becomes a way to assert your code does what you expect. After a few years you begin to use it as a design technique, and the correctness argument becomes less and less of a reason for using it. It's more of an (albeit nice) side effect at that point. I can write code that I test after the fact and still get the same correctness benefits, but the feedback I get from testing my design is gone.
Maybe I'm missing something, but I don't know if just having an excellent type checker is enough to provide the same quality feedback loop as well executed TDD does.
I've found this particularly useful when writing really confusing code (like a Prolog interpreter, for example). Coming up with the types on a function clarifies what it has to do and shrinks the space of possible solutions significantly.
Types are a symbolic way to reason about code. Using types, you can get additional insight into how your function can be written just by following some simple rules. A good example of this is realizing that a function you're working on is actually a specific version of a more general function--you can see this if the type signatures look similar. This lets you reuse very high-level, generic code easily.
Going back to the Prolog example, I was having some trouble figuring out how the resolution algorithm should work. Then I realized that the sub-part I was having problems with was just special type of fold. This helped me get a very concise version of the function by reusing an existing library function.
So types can provide exactly the same sort of benefits as TDD.
Happily, a new version of Hackage creatively called Hackage2 is being worked on which should ameliorate this problem (along with some other improvements). Improvement is just around the corner.
If someone's actually working on it again, that would be delightful.
Sorry, but that means you couldn't read it.
So, I still feel that understanding a piece of Haskell means that you will need to understand the individual functions at least superficially.