10 ms·

Confession of a Haskell Hacker

163 points by malloc47 14y ago

deleted 14y ago
[deleted]
spookylukey 14y ago
Why did you write it if you have never run it? Was it just for people who read your article and might want to run the code?
- VMG 14y ago
  Probably as an intellectual exercise.
  - hobin 14y ago
    But what point is there to an intellectual exercise if you don't know whether you've done it right in the end?
    - flatline3 14y ago
      That's the point of the article. The claim is that he knows he has done it right because the declarative types are simple enough to understand as a whole, and they enforce and ensure correctness, verified through compilation.
      - scott_s 14y ago
        Until the code has actually been tested, he doesn't know that it works, he just thinks that it does. The above point is that he has not completed the exercise, by verifying what he thinks.
        flatline3 14y ago
        The code was tested by the compiler, reducing the failure space to whether or not his declarative types are an adequate Proof. 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.
        scott_s 14y ago
        That's not good enough; you're still testing a proxy behavior, not the behavior under question. The hypothesis is, "Haskell's type system is robust enough that one can code an application through type checking alone." Doing the hypothesis is not testing the hypothesis; assuming the hypothesis is correct to demonstrate that the hypothesis is correct is begging the question. 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.
        flatline3 14y ago
        I object because you're attempting to extrapolate an axiom from an anecdote merely intended to demonstrates the value and power of the type system.
        scott_s 14y ago
        My point is we have not yet verified if the assumed conclusion of the anecdote is correct.
        wonderzombie 14y ago
        Consider that his Haskell program (ostensibly) relies on mathematical proofs, a chain of them. The compiler consumes and validates this chain of proofs and checks whether or not the program is "true." It's hard to imagine why you'd use the scientific method to verify that 1 + 1 + 1 == 3; basic math and logic--- something computers are good at--- are sufficient. 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.
        runeks 14y ago
        Ah yes, the old question of "what is knowledge?".
        JadeNB 14y ago
        > Until the code has actually been tested, he doesn't know that it works, he just thinks that it does. 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.)
        scott_s 14y ago
        I agree. I claim that he knows that it works under the circumstance that he has tested, and can be more confident that it will work in circumstances similar to what he has tested.
        zopa 14y ago
        True. But with very general code, like this library, it would be difficult for unit tests to cover more than a small fraction of the domain.
        tikhonj 14y ago
        Well, unless he has a proof that the code works. I think the idea is that, in this case, the types are so polymorphic that they do constitute a proof.
        scott_s 14y ago
        The insight behind Knuth's glib "I have only proved the program correct" quote is that proofs can still contain our untested assumptions. It's possible for someone to carry over an untested and wrong assumption from the implementation to the proof without ever finding out it is incorrect.
        tikhonj 14y ago
        Of course, the same is true for tests. If you prove the wrong thing, your code obviously won't be correct. If you test the wrong thing, your code obviously won't be correct. 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.
        scott_s 14y ago
        There's no way to prove that you proved the right thing, unfortunately. And, of course, your proof may not be correct. (Proof checkers can help, and I would have confidence in the correctness of a type-check as proof.) 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.
    - srparish 14y ago
      "Beware of bugs in the above code; I have only proved it correct, not tried it." -- Knuth
      - hobin 14y ago
        Touché. I see your point.
nothacker 14y ago
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. 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.
DanWaterworth 14y ago
I think the interesting point here is that Haskell provides such a high static assurance out of the box that what you write is correct that this can happen. You'd never hear of a ruby programmer releasing a gem without trying it.
- calpaterson 14y ago
  With the serious caveat that the program you are writing must only be vulnerable to the kind of errors which Hindley-Milner can show aren't present. ie: no IO, no non-deterministic concurrency, no non-total functions, etc, etc.
  - danieldk 14y ago
    In addition to that, it's often difficult to predict the runtime properties of a Haskell program. Due to it's laziness, one can often run into space leaks where thunks are not evaluated (yet): http://blog.ezyang.com/2011/05/space-leak-zoo/ http://blog.ezyang.com/2011/05/space-leak-zoo/
  - jeffdavis 14y ago
    You forgot the bug: "doesn't do what you want, but does it perfectly".
  - dwc 14y ago
    I wish this caveat were attached every time someone mentioned the "once it compiled it worked first time" bit. Not because there's no truth in the works-if-compiles idea, but because getting smug about it is sure to bite you in the ass sooner rather than later. 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.
batterseapower 14y ago
I find this happens a lot with Haskell. I can write hundreds of lines of code and have them work perfectly as soon as I get a error-free and warning-free compilation. 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.
- jlarocco 14y ago
  This just screams "bad development practice", IMO. 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...
  - statictype 14y ago
    Bad requirements and design errors can't be fixed by a perfect programming language. 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)
  - tikhonj 14y ago
    Haskell's type system can stop a ton of errors that would not be affected by a normal type system. I've certainly run into these sorts of errors in the wild. 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.
deleted 14y ago
[deleted]
Xion 14y ago
That's not very surprising; Haskell's type system is really that ridiculously powerful. But I suspect many hackers working with other languages would be able to state the equivalent: "I released a library which I only unit-tested, without writing any helper project that actually uses it".
- ludflu 14y ago
  except that they had to write unit tests - whereas the compiler/type system automatically checked the type safety of the code this guy wrote. (Not that writing unit tests for haskell code is a bad idea - QuickCheck is WAY more powerful than junits, for example)
  - Confusion 14y ago
    QuickCheck and JUnit have different purposes. QuickCheck is not a unit testing framework.
    - Xion 14y ago
      > QuickCheck and JUnit have different purposes. QuickCheck is not a unit testing framework. Indeed. What I meant was that basically: P(HaskellCodeCorrect|Compile+QC+UnitTest) =~= P(OtherCodeCorrect|Compile+UnitTest) while the distribution of effort between compilation (if any) and unit tests in other languages are quite different than in Haskell, i.e. skewed towards tests in the former and getting code to compile in the latter case.
aw3c2 14y ago
nothacker, you are "dead"/"ghosted". I am reposting his comment here: 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. 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.
- nothacker 14y ago
  Thanks! Have no idea if you or anyone else will see this, but appreciate the repost. I hope everyone will forgive me for the following aside, as it has little to do with the OP: Despite what PG and others think, there is a difference between troll and differing opinion. Unfortunately, since I buck authority and general consensus, I've lived in the shadows here ever since I was devmonk, a user that rose quickly in status, and then quit HN (changed password to something I could never retype and logged-out) when I realized I was addicted to it when someone else did the same thing. Unfortunately for me, PG, and HN, I can't stay away. I've written under so many different usernames and every time now I don't use a password I could ever retype, that way when I get tired of it, I logout never to login under that again. I like the community here and like to contribute. I would rather just post anonymously though. I think that any good system that relies on experience to promote thought can benefit from analytic criticism of some sort as long as any offense it causes is not permanently or long-wounding and does not limit beliefs or freedom. YC and PG unfortunately promote a sort of discussion that is slightly too limited. Reddit, Slashdot, and others are there for the "others", and HN for them is a place to act as an online part of YC that provides a way for "hackers" (though I hate the use of the term, as it invented it's own definition of "hacker") to share links, news, and science and discuss tech startups, SAAS apps, and ideas about tech startup entrepreneurship. That is fine, but what's also good is letting discussions manage themselves organically without axing dissenting opinion. In fact, the times that I've brought up how PG manages dissenting users, that gets shot down, too. Ok- maybe to some extent that is acceptable, to some extent, but a better way to handle it is by laying it out and saying each time, "I am making it harder on you to post by doing X because of Y." Anyway, just my 2 cents. Have a good one if you get this.
smcl 14y ago
Minor aside, is "I conjecture" valid English? I'm not criticising, just curious and in the pub.
- sneak 14y ago
  I believe so.
- lubutu 14y ago
  'Conjecture' is a verb as well as a noun. But I'll admit it sounds weird — by French inflection one would expect "I conject", which seems to be obsolete...
  - sigkill 14y ago
    Yep. Dictionary.com calls it obsolete. Webster wants me to pay, and OED can't find it. conject late 14c., obs. verb replaced by conjecture (v.). Also in form congette.
    - andrewcooke 14y ago
      my concise oxford dictionary (dead tree, c 1984) lists conjecture as a verb (not marked as obsolete).
      - tikhonj 14y ago
        It's the word "conject" that's obsolete, not "conjecture".
        andrewcooke 14y ago
        oh, sorry, mis-followed the conversation.
- Muzza 14y ago
  Very common in mathematical circles. Actually, the entire first page of Google's results for "we conjecture that" appears to be math.
smcl 14y ago
Minor aside, is "I conjecture" valid English? I'm not criticising, just curious and in the pub.
gosu 14y ago
Hindley-Milner is powerful, but there are usually multiple ways to construct a value of the correct type. Only one of those ways is the correct way, and I'd want to test my functional code to make sure that this was the way that I chose.
- JadeNB 14y ago
  As sanxiyn points out in http://news.ycombinator.com/item?id=4215055 http://news.ycombinator.com/item?id=4215055, although there are certainly many ways to produce a value of any concrete type, sufficient polymorphism will often guarantee (via the parametricity theorem) that there is only one total function of a specified type.
weeksie 14y ago
Ah, a Haskell circle-jerk waiting to happen and a confession that's really a way to act superior about Haskell's type system. Listen, it's a great language and I've spent a few years deep in it, but I find this post arrogant and not even accurate. 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.
- flatline3 14y ago
  I think your reply is inappropriately negative ("circle-jerk", "real world"), and that the negatively of your post detracts from what value might be derived from the article. 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.
  - weeksie 14y ago
    Well, I guess I'm just old enough and ugly enough to call things like I see them. Haskell is a neat language, but it is frustrating to listen to these sorts of brag-posts about the language because they're filled with dangerous hubris. The type system is amazing for certain kinds of problems. Hey, if you're writing a compiler then Haskell is probably the best language out there. Or in memory data structures. Hm. Or parsers. . . . It's a great language for CS research. 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.
    - Cieplak 14y ago
      Can you share some examples where you've found it to be a huge pain in the arse to use in production?
    - tikhonj 14y ago
      "Dangerous hubris" is an extremely condescending phrase. Do you think the author does not realize that the type system is only sufficient in certain, very specific cases? That's exactly what he mentions at the very end--the reason he trusted the type system so much is only because he believes there is only one non-trivial, non-recursive implementation with the requisite types. He qualifies exactly what he means and, moreover, does not even defend his behavior. And that is "dangerous hubris"? 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.
Cieplak 14y ago
What are functional lenses? http://www.haskellforall.com/2012/01/haskell-for-mainstream-programmers_28.html http://www.haskellforall.com/2012/01/haskell-for-mainstream-... http://stackoverflow.com/questions/8307370/functional-lenses http://stackoverflow.com/questions/8307370/functional-lenses
stewbrew 14y ago
As somebody who knows Haskell only superficially, this line of code and the author's statement makes me wonder if people can read their own or somebody else's code after some time.
- jrockway 14y ago
  Makes perfect sense to me.
- dwc 14y ago
  Yes, you can. I'm not a Haskell guru, and I haven't played with it in some time. I can read that line of code just fine. I don't actually know what it's doing, because I don't know the functions involved, etc., but the form of the line is easy enough to grok. Like any other language, it looks mysterious if you haven't read and written enough code in it, or in a language with a similar style.
  - dscrd 14y ago
    "I don't actually know what it's doing" Sorry, but that means you couldn't read it.
    - dwc 14y ago
      In a very real sense, that's true. But...I don't know what it's doing but I know how it's doing it, so to speak. With languages in which I'm quite fluent (Haskell not so much), I can sometimes spot problems in the code of someone coming to me for help without knowing anything about the libraries, et al, because even though I "couldn't read it" in your sense I could read it in the other sense.
    - papsosouid 14y ago
      No it doesn't: foo(bar(x)) Can you read that code? Yes? But you don't know what it is doing, because you don't know what the functions foo and bar do. Same deal with the haskell code in question. Just because you don't know what Compose and getCompose do, doesn't mean you can't read the code.
sanxiyn 14y ago
This is supported by the parametricity theorem. That is a big word, but it boils down to this: let's say you wrote an identity function of type "a -> a", and it passed the type checker. Then it is correct: you simply can't do much with a value of type "a", because you don't know anything about it. 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.
- MaleKitten 14y ago
  Types are propositions, and programs are proofs. If your program satisfies the type, then it is a proof of the proposition.
  - cwzwarich 14y ago
    In Haskell all types are inhabited, so every proposition has a proof. This makes Haskell a pretty useless logic.
    - deleted 14y ago
      [deleted]
    - rpearl 14y ago
      Some of them are only inhabited by bottom, no? I cannot write down a function f :: a -> b besides: f :: a -> b f = undefined
      - cwzwarich 14y ago
        There are a lot of other Haskell features you can use. Term-level recursion works: f :: a -> b f = f Type-level recursion works, even without explicit term-level recursion: 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) This is basically encoding Russell's paradox at the type level. You can write out f explicitly, just so that it doesn't look like you might somehow still be applying w to itself recursively: g :: a -> b g = (\x -> ((\(C f) -> f) x) x) (C (\x -> ((\(C f) -> f) x) x)) There are even ways of doing this using highly impredicative definitions involving GADTs and type families, without involving any explicit recursion at all: http://okmij.org/ftp/Haskell/impredicativity-bites.html http://okmij.org/ftp/Haskell/impredicativity-bites.html 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.
jlarocco 14y ago
And that's something he's proud of? 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.
sanxiyn 14y ago
From the article: "The types are so polymorphic that I conjecture that there is only one way to write functions matching the required types such that all parameters are used non-trivially and recursion is not used." 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.
anothermachine 14y ago
This is why Hackage is full of junk and Haskell is unapproachable for real-world projects. Everyone's throwaway toy file is published as a package, and the useful well-documented packages get lost in the mix.
- tikhonj 14y ago
  Ignoring the baseless FUD in the first part of your post, your last point is actually valid: it is hard to find good, maintained packages on Hackage. Right now the standard solution seems to be just asking somebody with more experience, but this is clearly not scalable. 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.
  - anothermachine 14y ago
    Hackage2 has been around the corner for years. The "public testing instance" doesn't exist. http://hackage.haskell.org/trac/hackage/wiki/HackageDB/2.0 http://hackage.haskell.org/trac/hackage/wiki/HackageDB/2.0 If someone's actually working on it again, that would be delightful.
crntaylor 14y ago
This post is a representative of everything that I both love and hate about Haskell: 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.
- djhworld 14y ago
  Your description on deleting files not being protected by the type system is the result of side effects at runtime. The point of the OP was discussing the safety that can be achieved from pure code.
  - crntaylor 14y ago
    I feel like I addressed this fully in my comment. I agree with the OP - you can do great things with the Haskell type system, if you're writing pure code and if you're writing sufficiently polymorphic code. I think this is awesome! 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.
dkubb 14y ago
As someone who is interesting in writing more Haskell, I've heard all the "if I get it to compile it works perfectly the first time", and I wonder if people are missing out on what proper TDD can bring them. 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.
- tikhonj 14y ago
  You can use the types the same way--define your types and write type signatures for your functions before implementing them. 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.

163 points by malloc47 14y ago

deleted 14y ago

[deleted]

Why did you write it if you have never run it? Was it just for people who read your article and might want to run the code?

VMG 14y ago
Probably as an intellectual exercise.
- hobin 14y ago
  But what point is there to an intellectual exercise if you don't know whether you've done it right in the end?
  - flatline3 14y ago
    That's the point of the article. The claim is that he knows he has done it right because the declarative types are simple enough to understand as a whole, and they enforce and ensure correctness, verified through compilation.
    - scott_s 14y ago
      Until the code has actually been tested, he doesn't know that it works, he just thinks that it does. The above point is that he has not completed the exercise, by verifying what he thinks.
      - flatline3 14y ago
        The code was tested by the compiler, reducing the failure space to whether or not his declarative types are an adequate Proof. 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.
        scott_s 14y ago
        That's not good enough; you're still testing a proxy behavior, not the behavior under question. The hypothesis is, "Haskell's type system is robust enough that one can code an application through type checking alone." Doing the hypothesis is not testing the hypothesis; assuming the hypothesis is correct to demonstrate that the hypothesis is correct is begging the question. 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.
        flatline3 14y ago
        I object because you're attempting to extrapolate an axiom from an anecdote merely intended to demonstrates the value and power of the type system.
        scott_s 14y ago
        My point is we have not yet verified if the assumed conclusion of the anecdote is correct.
        wonderzombie 14y ago
        Consider that his Haskell program (ostensibly) relies on mathematical proofs, a chain of them. The compiler consumes and validates this chain of proofs and checks whether or not the program is "true." It's hard to imagine why you'd use the scientific method to verify that 1 + 1 + 1 == 3; basic math and logic--- something computers are good at--- are sufficient. 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.
      - runeks 14y ago
        Ah yes, the old question of "what is knowledge?".
      - JadeNB 14y ago
        > Until the code has actually been tested, he doesn't know that it works, he just thinks that it does. 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.)
        scott_s 14y ago
        I agree. I claim that he knows that it works under the circumstance that he has tested, and can be more confident that it will work in circumstances similar to what he has tested.
        zopa 14y ago
        True. But with very general code, like this library, it would be difficult for unit tests to cover more than a small fraction of the domain.
      - tikhonj 14y ago
        Well, unless he has a proof that the code works. I think the idea is that, in this case, the types are so polymorphic that they do constitute a proof.
        scott_s 14y ago
        The insight behind Knuth's glib "I have only proved the program correct" quote is that proofs can still contain our untested assumptions. It's possible for someone to carry over an untested and wrong assumption from the implementation to the proof without ever finding out it is incorrect.
        tikhonj 14y ago
        Of course, the same is true for tests. If you prove the wrong thing, your code obviously won't be correct. If you test the wrong thing, your code obviously won't be correct. 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.
        scott_s 14y ago
        There's no way to prove that you proved the right thing, unfortunately. And, of course, your proof may not be correct. (Proof checkers can help, and I would have confidence in the correctness of a type-check as proof.) 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.
  - srparish 14y ago
    "Beware of bugs in the above code; I have only proved it correct, not tried it." -- Knuth
    - hobin 14y ago
      Touché. I see your point.

nothacker 14y ago

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

DanWaterworth 14y ago

I think the interesting point here is that Haskell provides such a high static assurance out of the box that what you write is correct that this can happen. You'd never hear of a ruby programmer releasing a gem without trying it.

calpaterson 14y ago
With the serious caveat that the program you are writing must only be vulnerable to the kind of errors which Hindley-Milner can show aren't present. ie: no IO, no non-deterministic concurrency, no non-total functions, etc, etc.
- danieldk 14y ago
  In addition to that, it's often difficult to predict the runtime properties of a Haskell program. Due to it's laziness, one can often run into space leaks where thunks are not evaluated (yet): http://blog.ezyang.com/2011/05/space-leak-zoo/ http://blog.ezyang.com/2011/05/space-leak-zoo/
- jeffdavis 14y ago
  You forgot the bug: "doesn't do what you want, but does it perfectly".
- dwc 14y ago
  I wish this caveat were attached every time someone mentioned the "once it compiled it worked first time" bit. Not because there's no truth in the works-if-compiles idea, but because getting smug about it is sure to bite you in the ass sooner rather than later. 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.

batterseapower 14y ago

I find this happens a lot with Haskell. I can write hundreds of lines of code and have them work perfectly as soon as I get a error-free and warning-free compilation. 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.

jlarocco 14y ago
This just screams "bad development practice", IMO. 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...
- statictype 14y ago
  Bad requirements and design errors can't be fixed by a perfect programming language. 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)
- tikhonj 14y ago
  Haskell's type system can stop a ton of errors that would not be affected by a normal type system. I've certainly run into these sorts of errors in the wild. 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.

deleted 14y ago

[deleted]

Xion 14y ago

That's not very surprising; Haskell's type system is really that ridiculously powerful. But I suspect many hackers working with other languages would be able to state the equivalent: "I released a library which I only unit-tested, without writing any helper project that actually uses it".

ludflu 14y ago
except that they had to write unit tests - whereas the compiler/type system automatically checked the type safety of the code this guy wrote. (Not that writing unit tests for haskell code is a bad idea - QuickCheck is WAY more powerful than junits, for example)
- Confusion 14y ago
  QuickCheck and JUnit have different purposes. QuickCheck is not a unit testing framework.
  - Xion 14y ago
    > QuickCheck and JUnit have different purposes. QuickCheck is not a unit testing framework. Indeed. What I meant was that basically: P(HaskellCodeCorrect|Compile+QC+UnitTest) =~= P(OtherCodeCorrect|Compile+UnitTest) while the distribution of effort between compilation (if any) and unit tests in other languages are quite different than in Haskell, i.e. skewed towards tests in the former and getting code to compile in the latter case.

aw3c2 14y ago

nothacker, you are "dead"/"ghosted". I am reposting his comment here: 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. 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.

nothacker 14y ago
Thanks! Have no idea if you or anyone else will see this, but appreciate the repost. I hope everyone will forgive me for the following aside, as it has little to do with the OP: Despite what PG and others think, there is a difference between troll and differing opinion. Unfortunately, since I buck authority and general consensus, I've lived in the shadows here ever since I was devmonk, a user that rose quickly in status, and then quit HN (changed password to something I could never retype and logged-out) when I realized I was addicted to it when someone else did the same thing. Unfortunately for me, PG, and HN, I can't stay away. I've written under so many different usernames and every time now I don't use a password I could ever retype, that way when I get tired of it, I logout never to login under that again. I like the community here and like to contribute. I would rather just post anonymously though. I think that any good system that relies on experience to promote thought can benefit from analytic criticism of some sort as long as any offense it causes is not permanently or long-wounding and does not limit beliefs or freedom. YC and PG unfortunately promote a sort of discussion that is slightly too limited. Reddit, Slashdot, and others are there for the "others", and HN for them is a place to act as an online part of YC that provides a way for "hackers" (though I hate the use of the term, as it invented it's own definition of "hacker") to share links, news, and science and discuss tech startups, SAAS apps, and ideas about tech startup entrepreneurship. That is fine, but what's also good is letting discussions manage themselves organically without axing dissenting opinion. In fact, the times that I've brought up how PG manages dissenting users, that gets shot down, too. Ok- maybe to some extent that is acceptable, to some extent, but a better way to handle it is by laying it out and saying each time, "I am making it harder on you to post by doing X because of Y." Anyway, just my 2 cents. Have a good one if you get this.

smcl 14y ago

Minor aside, is "I conjecture" valid English? I'm not criticising, just curious and in the pub.

sneak 14y ago
I believe so.
lubutu 14y ago
'Conjecture' is a verb as well as a noun. But I'll admit it sounds weird — by French inflection one would expect "I conject", which seems to be obsolete...
- sigkill 14y ago
  Yep. Dictionary.com calls it obsolete. Webster wants me to pay, and OED can't find it. conject late 14c., obs. verb replaced by conjecture (v.). Also in form congette.
  - andrewcooke 14y ago
    my concise oxford dictionary (dead tree, c 1984) lists conjecture as a verb (not marked as obsolete).
    - tikhonj 14y ago
      It's the word "conject" that's obsolete, not "conjecture".
      - andrewcooke 14y ago
        oh, sorry, mis-followed the conversation.
Muzza 14y ago
Very common in mathematical circles. Actually, the entire first page of Google's results for "we conjecture that" appears to be math.

smcl 14y ago

Minor aside, is "I conjecture" valid English? I'm not criticising, just curious and in the pub.

gosu 14y ago

Hindley-Milner is powerful, but there are usually multiple ways to construct a value of the correct type. Only one of those ways is the correct way, and I'd want to test my functional code to make sure that this was the way that I chose.

JadeNB 14y ago
As sanxiyn points out in http://news.ycombinator.com/item?id=4215055 http://news.ycombinator.com/item?id=4215055, although there are certainly many ways to produce a value of any concrete type, sufficient polymorphism will often guarantee (via the parametricity theorem) that there is only one total function of a specified type.

weeksie 14y ago

Ah, a Haskell circle-jerk waiting to happen and a confession that's really a way to act superior about Haskell's type system. Listen, it's a great language and I've spent a few years deep in it, but I find this post arrogant and not even accurate. 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.

flatline3 14y ago
I think your reply is inappropriately negative ("circle-jerk", "real world"), and that the negatively of your post detracts from what value might be derived from the article. 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.
- weeksie 14y ago
  Well, I guess I'm just old enough and ugly enough to call things like I see them. Haskell is a neat language, but it is frustrating to listen to these sorts of brag-posts about the language because they're filled with dangerous hubris. The type system is amazing for certain kinds of problems. Hey, if you're writing a compiler then Haskell is probably the best language out there. Or in memory data structures. Hm. Or parsers. . . . It's a great language for CS research. 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.
  - Cieplak 14y ago
    Can you share some examples where you've found it to be a huge pain in the arse to use in production?
  - tikhonj 14y ago
    "Dangerous hubris" is an extremely condescending phrase. Do you think the author does not realize that the type system is only sufficient in certain, very specific cases? That's exactly what he mentions at the very end--the reason he trusted the type system so much is only because he believes there is only one non-trivial, non-recursive implementation with the requisite types. He qualifies exactly what he means and, moreover, does not even defend his behavior. And that is "dangerous hubris"? 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.

Cieplak 14y ago

What are functional lenses? http://www.haskellforall.com/2012/01/haskell-for-mainstream-programmers_28.html http://www.haskellforall.com/2012/01/haskell-for-mainstream-... http://stackoverflow.com/questions/8307370/functional-lenses http://stackoverflow.com/questions/8307370/functional-lenses

stewbrew 14y ago

As somebody who knows Haskell only superficially, this line of code and the author's statement makes me wonder if people can read their own or somebody else's code after some time.

jrockway 14y ago
Makes perfect sense to me.
dwc 14y ago
Yes, you can. I'm not a Haskell guru, and I haven't played with it in some time. I can read that line of code just fine. I don't actually know what it's doing, because I don't know the functions involved, etc., but the form of the line is easy enough to grok. Like any other language, it looks mysterious if you haven't read and written enough code in it, or in a language with a similar style.
- dscrd 14y ago
  "I don't actually know what it's doing" Sorry, but that means you couldn't read it.
  - dwc 14y ago
    In a very real sense, that's true. But...I don't know what it's doing but I know how it's doing it, so to speak. With languages in which I'm quite fluent (Haskell not so much), I can sometimes spot problems in the code of someone coming to me for help without knowing anything about the libraries, et al, because even though I "couldn't read it" in your sense I could read it in the other sense.
  - papsosouid 14y ago
    No it doesn't: foo(bar(x)) Can you read that code? Yes? But you don't know what it is doing, because you don't know what the functions foo and bar do. Same deal with the haskell code in question. Just because you don't know what Compose and getCompose do, doesn't mean you can't read the code.

sanxiyn 14y ago

This is supported by the parametricity theorem. That is a big word, but it boils down to this: let's say you wrote an identity function of type "a -> a", and it passed the type checker. Then it is correct: you simply can't do much with a value of type "a", because you don't know anything about it. 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.

MaleKitten 14y ago
Types are propositions, and programs are proofs. If your program satisfies the type, then it is a proof of the proposition.
- cwzwarich 14y ago
  In Haskell all types are inhabited, so every proposition has a proof. This makes Haskell a pretty useless logic.
  - deleted 14y ago
    [deleted]
  - rpearl 14y ago
    Some of them are only inhabited by bottom, no? I cannot write down a function f :: a -> b besides: f :: a -> b f = undefined
    - cwzwarich 14y ago
      There are a lot of other Haskell features you can use. Term-level recursion works: f :: a -> b f = f Type-level recursion works, even without explicit term-level recursion: 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) This is basically encoding Russell's paradox at the type level. You can write out f explicitly, just so that it doesn't look like you might somehow still be applying w to itself recursively: g :: a -> b g = (\x -> ((\(C f) -> f) x) x) (C (\x -> ((\(C f) -> f) x) x)) There are even ways of doing this using highly impredicative definitions involving GADTs and type families, without involving any explicit recursion at all: http://okmij.org/ftp/Haskell/impredicativity-bites.html http://okmij.org/ftp/Haskell/impredicativity-bites.html 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.

jlarocco 14y ago

And that's something he's proud of? 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.

sanxiyn 14y ago

From the article: "The types are so polymorphic that I conjecture that there is only one way to write functions matching the required types such that all parameters are used non-trivially and recursion is not used." 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.

anothermachine 14y ago

This is why Hackage is full of junk and Haskell is unapproachable for real-world projects. Everyone's throwaway toy file is published as a package, and the useful well-documented packages get lost in the mix.

tikhonj 14y ago
Ignoring the baseless FUD in the first part of your post, your last point is actually valid: it is hard to find good, maintained packages on Hackage. Right now the standard solution seems to be just asking somebody with more experience, but this is clearly not scalable. 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.
- anothermachine 14y ago
  Hackage2 has been around the corner for years. The "public testing instance" doesn't exist. http://hackage.haskell.org/trac/hackage/wiki/HackageDB/2.0 http://hackage.haskell.org/trac/hackage/wiki/HackageDB/2.0 If someone's actually working on it again, that would be delightful.

crntaylor 14y ago

This post is a representative of everything that I both love and hate about Haskell: 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.

djhworld 14y ago
Your description on deleting files not being protected by the type system is the result of side effects at runtime. The point of the OP was discussing the safety that can be achieved from pure code.
- crntaylor 14y ago
  I feel like I addressed this fully in my comment. I agree with the OP - you can do great things with the Haskell type system, if you're writing pure code and if you're writing sufficiently polymorphic code. I think this is awesome! 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.

dkubb 14y ago

As someone who is interesting in writing more Haskell, I've heard all the "if I get it to compile it works perfectly the first time", and I wonder if people are missing out on what proper TDD can bring them. 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.

tikhonj 14y ago
You can use the types the same way--define your types and write type signatures for your functions before implementing them. 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.