8 ms·

Haskell Is Exceptionally Unsafe (2012)

107 points by kirkbackus 12y ago

bjterry 12y ago
There was some discussion on this topic a while back which I remember. For convenience, it is linked here: https://news.ycombinator.com/item?id=4380900 https://news.ycombinator.com/item?id=4380900
carterschonwald 12y ago
I'd like to point out that the example at the end of the blog post is only runnable in GHC 7.6 and Older. As of GHC 7.8, you can't define your own custom typeable methods, you can only ask GHC to derive a typeable instance
coolsunglasses 12y ago
Harper's an accomplished person in CS and has done great work, but he's not putting a good argument forward here. I've talked to Harper about this post and his opposition to Haskell before. I mentioned that it was leading people to believe they could ignore typed FP, not redirecting to an ML derivative. Harper expressed dismay at this. There are more advanced languages than Haskell, they aren't ML, and PL researchers/experimenters are still working out how to make them work nicely for day to day stuff. First: http://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf http://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loos... (This isn't a throw-away reference, informal reasoning has worked extremely well in practice. Yes, I'm making that argument as a user of a pure, typed FP language.) unsafePerformIO is primarily used to change thunk-memoization behavior [1]. Also, it says unsafe right on the tin. Nobody uses it in practice in ordinary code. It's not something you have to incorporate when reasoning about code. Giving up reasoning about your Haskell code as if there were semantics-violating unsafePerformIOs lurking in the depths is similar to giving up reasoning about any code because a cosmic ray might flip a bit. Lets consider the rather remarkable backflips Standard ML and OCaml had to perform in order to make FP work with strictness and impurity. You can ignore unsafePerformIO because very very few people ever need it and you'll almost never have a reason to use it. Just don't use it. Similarly, writing total functions is the cultural default in Haskell. The compiler warns on incomplete pattern matches which you can -Werror as well. You can't define your own Typeable instances as of GHC 7.8 - only derive them, so that soundness issue is gone. Typeable itself is not popularly used, particularly as SYB has fallen out of favor. One critical aspect of why I like Haskell and the community around it is the willingness to fix mistakes. Meanwhile, ML implementations still use the value restriction. >the example once again calls into question the dogma Oh please. Haskell is an ensemble, multi-paradigm language with the right defaults (purity, types, immutability, expressions-only) and escape hatches for when you need them. Haskellers appreciate the value of modules a la ML, but typeclasses and polymorphism by default have proven more compelling in the majority of use-cases. There are still some situations where modules (fibration) would be preferred without resorting to explicit records of functions. For those cases, Backpack [3] is in the works. It won't likely satisfy serious ML users, but should hopefully clean up gaps Haskell users have identified on their own. Harper's case is over-stated, outdated, and not graced with an understanding of how Haskell code is written. Informal reasoning works if the foundations (purity, types, FP) are solid. [1]: https://github.com/bitemyapp/blacktip/blob/master/src/Database/Blacktip.hs#L47-L54 https://github.com/bitemyapp/blacktip/blob/master/src/Databa... [2]: http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf http://caml.inria.fr/pub/papers/garrigue-value_restriction-f... [3]: http://plv.mpi-sws.org/backpack/ http://plv.mpi-sws.org/backpack/
- thirsteh 12y ago
  Having read numerous rants by Harper against Haskell, it really just seems like he's upset Haskell turned out to be the "popular" language. He is an accomplished computer scientist and a major contributor to Standard ML (i.e. understandably biased), but his Haskell rants read like (type-safe) schoolyard banter.
  - peterfirefly 12y ago
    Usually Andreas Rossberger has written a good rebuttal in the comments.
  - tel 12y ago
    Perhaps there are some sour grapes, but I think more than that he's just hoping for more. Harper clearly has an executes on a grand vision for what PLs should be—he regularly states that there is only one PL and we're just working to slowly uncover it. Haskell fits it in some ways, and now those ways aren't worth talking about any further, and misses it in others. Harper, I believe, writes to galvanize people to move toward his grand vision of unified PL. ML is better than Haskell in many ways. This should drive Haskell to improve as much as it drives people to check out ML. And it has!
    - thirsteh 12y ago
      That makes sense. I wish he'd stop writing obviously linkbait titles like "Haskell is Exceptionally Unsafe" when what he means is that there are some really obscure safety implications for typeable exceptions. I completely agree with bjterry that it has probably caused more people to not look at Haskell to begin with, than people to look at ML.
      - tel 12y ago
        I think, honestly, Harper has recently discovered his platform is larger than he once expected. There was certainly a time that incendiary, link-Barry titles were useful for, say, getting Haskell's exception system to be more safe (which he absolutely played a part in). As the audience of his posts widens though it's clear that the impact of those posts is changing.
jonsterling 12y ago
As others have said, it's not nearly as bad anymore as It was when Bob wrote that post, but I would say, please do not take that as a reason to not take what he says very seriously. I use haskell because it is a very practical tool, (bona fides: I am an experienced haskell developer and I actually use it full time for my job---not an armchair evangelist) but it has become very clear to me that the next great thing will be more like ML than like Haskell. There are of course many important lessons to be learned from Haskell though!
- bronxbomber92 12y ago
  Could you expand on why you think the next "great thing" will be more like ML than like Haskell?
  - jonsterling 12y ago
    1. Call-by-value gives us both the ability reason by induction. It also typically results in the presence of non-pointed types, whereas Haskell only has pointed types. 2. Call-by-value gives us the ability to safely interleave effects. Now, I know you all think we should not be doing that at all, but I would say that this is only true in some cases. The point of reifying an effect in a monad is not because "effects are icky"; it is because we have written a non-extensional operation using effects, and we want it to be an extensional function. Wrapping it up in the monad "completes" the operation as such. However, there are plenty of extensional functions which may be written using computational effects (such as memoization): these should not be wrapped up in the monad. (FYI, it's the effects that preserve extensionality which is what Bob calls "benign effects", to the consternation of Haskell developers everywhere.) ML gives us the fine-grainedness to make these choices, at the cost of some reasoning facilities: more proofs must be done on paper, or in an external logical framework. I tend to think that the latter is inevitable, but some disagree. I am hoping for a middle-ground then: something like ML, in that effects are fundamental and not just bolted onto the language with a stack of monads; something like Haskell, where we can tell what effects are being used by a piece of code. The story hasn't been fully written on this, but I think that Call-by-push-value can help us with both recovering the benefits of laziness as well as reasoning about effects. 3. Modularity is something which Haskell people simply do not take seriously, even with the new "backpack" package-level module system they are building. One of the most-loved reasoning facilities present in Haskell depends, believe it or not, on global scope, and is therefore inherently anti-modular (this is the uniqueness of type class instances). As a result, you can never add modularity to Haskell, but we may be able to back-port some of the more beloved aspects of Haskell to a new nephew in the ML family. (Confusingly, laziness advocates often say that their brand of functional programming has better "modularity" than strict, because of the way that you can compose lazy algorithms to get more lazy algorithms that don't totally blow up in complexity. I would say that lazy languages are more "compositional", not more "modular"—I prefer to use the latter term for modularity at the level of architecture and systems design, not algorithms.)
wyager 12y ago
>The most blatant violation is the all too necessary, but aptly named, unsafePerformIO The only time it's necessary is when you're using the FFI or working with language internals, at which point there's really no way for the type checker to work anyway. One should avoid using exceptions in pure code. This is well established. Instead, use any of the many type-safe exception mechanisms, like Maybe or Either. Having written probably in the high thousands or low tens of thousands of LoC of Haskell, I've never once used a user-defined exception or undefined. The point of this article seems to be "If your code breaks, it's no longer type safe.". I don't think this is news to anyone.
- mercurial 12y ago
  > Having written probably in the high thousands or low tens of thousands of LoC of Haskell, I've never once used a user-defined exception or undefined. Good for you, I guess. You'll find plenty of libraries which have no qualms about using exceptions in the real world, though. Not to mention asynchronous exceptions, obviously. Personally, I find both exceptions and type-safe error handling unsatisfactory. The former is unsafe, the latter results usually in a "god error type" which breaks modularity.
  - wyager 12y ago
    >plenty of libraries which have no qualms about using exceptions in the real world I haven't run into too many (particularly when compared to the popularity of exceptions in other languages). >the latter results usually in a "god error type" which breaks modularity. Have you tried using Either with a sum error type and/or an error typeclass?
    - mercurial 12y ago
      > I haven't run into too many (particularly when compared to the popularity of exceptions in other languages). This doesn't mean much if you take a language like Java where it is the idiomatic way of handling errors. But take something vaguely complex like http-client (formerly http-conduit) and you get exceptions. > Have you tried using Either with a sum error type and/or an error typeclass? Well, even with sum types you get "god errors" which encapsulate all kinds of issues that can happen in your exception, because it's the path of least resistance. I haven't tried Either with a typeclass, though, but it sounds vaguely abusive.
tailrecursion 12y ago
I want to question the importance of soundness in type systems. Suppose you could catch 99% of type-based errors instead of 100%, and in addition, use a compiler switch to see all the case statements where a class of a type is missing. The intended benefit of this system is that it accepts all correct programs. Correct meaning, the program runs and returns the correct answer. Would such a language be viable? Or is it absolutely necessary to catch all possible type errors. In the past, tools like lint have been considered useful, although lint is not at all the kind of type system that I envision, namely a system that is in practice catching all the errors that ML catches -- it just doesn't (and cannot) guarantee it catches them. The restrictive nature of static type systems today is legendary, but I wonder sometimes whether people realize how restrictive they are. If you can't make your idea work with functors or typeclasses, chances are good there's no way to get it to compile and you have to write functions in longhand.
- shadowfox 12y ago
  There is always idea of Gradual Typing [1] which has been implemented with varying degrees of success. There are also a large set of static analysis theories/tools which can help here. It is also worth noting that if you dont want (global) type inference, you can get far in a language with permissive casting, type annotations and local inference. The results aren't a panacea though. > Suppose you could catch 99% of type-based errors instead of 100%, and in addition, use a compiler switch to see all the case statements where a class of a type is missing. I am not quite sure what you mean by this. Care to elaborate? (In general, with inference systems, missing type information is hard(ish) to localize. So pointing out where exactly a type error occurred is non-trivial) [1] https://en.wikipedia.org/wiki/Gradual_typing https://en.wikipedia.org/wiki/Gradual_typing
  - tailrecursion 12y ago
    I'm thinking of a system with valueset inference where valuesets are not necessarily disjoint. So the system may infer that a return value is the disjunction {INTEGER | REAL}. In order to get precision in checking, a lot of computation needs to be done so the compiler relaxes the precision when facing large disjunctions (networks) of constraints. Dynamic checks are inserted as necessary but a system that relaxes when things get hairy can't guarantee that it will find all errors at compile time. The idea is similar to Soft Typing of Cartwright and others, but they were thinking of an interactive system, some kind of programmer's aid. If I recall they ran into problems giving reasonable error messages.
accessright 12y ago
So basically it is "unsafePerformIO" and "error" that is the problem? So if you do not use them (which I never do and it is recommended not to) then the problem is not relevant?
- densh 12y ago
  I think the main problem here is that it's not just you, but also your transitive dependencies.
- Lambdanaut 12y ago
  It seems to me that it would also be any function you import that uses these. Unfortunately, there are a lot of very commonly used functions that use `error`.
qwerta 12y ago
Being unsafe never stopped Ruby or PHP, while Ada is still nowhere.
- CmonDev 12y ago
  "never stopped Ruby or PHP" Lots of poorly-maintainable code is a good thing?
- Horusiath 12y ago
  Tell that next time you get on the plane.
- progman 12y ago
  http://www.ada2012.org http://www.ada2012.org
- praptak 12y ago
  This misses the point. Statically typed functional languages. Safety is the selling point here.
reirob 12y ago
Here the reddit thread about this article, from 2 years ago: http://www.reddit.com/r/haskell/comments/y74vn/robert_harper_haskell_is_exceptionally_unsafe/?already_submitted=true http://www.reddit.com/r/haskell/comments/y74vn/robert_harper...

107 points by kirkbackus 12y ago

There was some discussion on this topic a while back which I remember. For convenience, it is linked here: https://news.ycombinator.com/item?id=4380900 https://news.ycombinator.com/item?id=4380900

carterschonwald 12y ago

I'd like to point out that the example at the end of the blog post is only runnable in GHC 7.6 and Older. As of GHC 7.8, you can't define your own custom typeable methods, you can only ask GHC to derive a typeable instance

coolsunglasses 12y ago

Harper's an accomplished person in CS and has done great work, but he's not putting a good argument forward here. I've talked to Harper about this post and his opposition to Haskell before. I mentioned that it was leading people to believe they could ignore typed FP, not redirecting to an ML derivative. Harper expressed dismay at this. There are more advanced languages than Haskell, they aren't ML, and PL researchers/experimenters are still working out how to make them work nicely for day to day stuff. First: http://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf http://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loos... (This isn't a throw-away reference, informal reasoning has worked extremely well in practice. Yes, I'm making that argument as a user of a pure, typed FP language.) unsafePerformIO is primarily used to change thunk-memoization behavior [1]. Also, it says unsafe right on the tin. Nobody uses it in practice in ordinary code. It's not something you have to incorporate when reasoning about code. Giving up reasoning about your Haskell code as if there were semantics-violating unsafePerformIOs lurking in the depths is similar to giving up reasoning about any code because a cosmic ray might flip a bit. Lets consider the rather remarkable backflips Standard ML and OCaml had to perform in order to make FP work with strictness and impurity. You can ignore unsafePerformIO because very very few people ever need it and you'll almost never have a reason to use it. Just don't use it. Similarly, writing total functions is the cultural default in Haskell. The compiler warns on incomplete pattern matches which you can -Werror as well. You can't define your own Typeable instances as of GHC 7.8 - only derive them, so that soundness issue is gone. Typeable itself is not popularly used, particularly as SYB has fallen out of favor. One critical aspect of why I like Haskell and the community around it is the willingness to fix mistakes. Meanwhile, ML implementations still use the value restriction. >the example once again calls into question the dogma Oh please. Haskell is an ensemble, multi-paradigm language with the right defaults (purity, types, immutability, expressions-only) and escape hatches for when you need them. Haskellers appreciate the value of modules a la ML, but typeclasses and polymorphism by default have proven more compelling in the majority of use-cases. There are still some situations where modules (fibration) would be preferred without resorting to explicit records of functions. For those cases, Backpack [3] is in the works. It won't likely satisfy serious ML users, but should hopefully clean up gaps Haskell users have identified on their own. Harper's case is over-stated, outdated, and not graced with an understanding of how Haskell code is written. Informal reasoning works if the foundations (purity, types, FP) are solid. [1]: https://github.com/bitemyapp/blacktip/blob/master/src/Database/Blacktip.hs#L47-L54 https://github.com/bitemyapp/blacktip/blob/master/src/Databa... [2]: http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf http://caml.inria.fr/pub/papers/garrigue-value_restriction-f... [3]: http://plv.mpi-sws.org/backpack/ http://plv.mpi-sws.org/backpack/

thirsteh 12y ago
Having read numerous rants by Harper against Haskell, it really just seems like he's upset Haskell turned out to be the "popular" language. He is an accomplished computer scientist and a major contributor to Standard ML (i.e. understandably biased), but his Haskell rants read like (type-safe) schoolyard banter.
- peterfirefly 12y ago
  Usually Andreas Rossberger has written a good rebuttal in the comments.
- tel 12y ago
  Perhaps there are some sour grapes, but I think more than that he's just hoping for more. Harper clearly has an executes on a grand vision for what PLs should be—he regularly states that there is only one PL and we're just working to slowly uncover it. Haskell fits it in some ways, and now those ways aren't worth talking about any further, and misses it in others. Harper, I believe, writes to galvanize people to move toward his grand vision of unified PL. ML is better than Haskell in many ways. This should drive Haskell to improve as much as it drives people to check out ML. And it has!
  - thirsteh 12y ago
    That makes sense. I wish he'd stop writing obviously linkbait titles like "Haskell is Exceptionally Unsafe" when what he means is that there are some really obscure safety implications for typeable exceptions. I completely agree with bjterry that it has probably caused more people to not look at Haskell to begin with, than people to look at ML.
    - tel 12y ago
      I think, honestly, Harper has recently discovered his platform is larger than he once expected. There was certainly a time that incendiary, link-Barry titles were useful for, say, getting Haskell's exception system to be more safe (which he absolutely played a part in). As the audience of his posts widens though it's clear that the impact of those posts is changing.

jonsterling 12y ago

As others have said, it's not nearly as bad anymore as It was when Bob wrote that post, but I would say, please do not take that as a reason to not take what he says very seriously. I use haskell because it is a very practical tool, (bona fides: I am an experienced haskell developer and I actually use it full time for my job---not an armchair evangelist) but it has become very clear to me that the next great thing will be more like ML than like Haskell. There are of course many important lessons to be learned from Haskell though!

bronxbomber92 12y ago
Could you expand on why you think the next "great thing" will be more like ML than like Haskell?
- jonsterling 12y ago
  1. Call-by-value gives us both the ability reason by induction. It also typically results in the presence of non-pointed types, whereas Haskell only has pointed types. 2. Call-by-value gives us the ability to safely interleave effects. Now, I know you all think we should not be doing that at all, but I would say that this is only true in some cases. The point of reifying an effect in a monad is not because "effects are icky"; it is because we have written a non-extensional operation using effects, and we want it to be an extensional function. Wrapping it up in the monad "completes" the operation as such. However, there are plenty of extensional functions which may be written using computational effects (such as memoization): these should not be wrapped up in the monad. (FYI, it's the effects that preserve extensionality which is what Bob calls "benign effects", to the consternation of Haskell developers everywhere.) ML gives us the fine-grainedness to make these choices, at the cost of some reasoning facilities: more proofs must be done on paper, or in an external logical framework. I tend to think that the latter is inevitable, but some disagree. I am hoping for a middle-ground then: something like ML, in that effects are fundamental and not just bolted onto the language with a stack of monads; something like Haskell, where we can tell what effects are being used by a piece of code. The story hasn't been fully written on this, but I think that Call-by-push-value can help us with both recovering the benefits of laziness as well as reasoning about effects. 3. Modularity is something which Haskell people simply do not take seriously, even with the new "backpack" package-level module system they are building. One of the most-loved reasoning facilities present in Haskell depends, believe it or not, on global scope, and is therefore inherently anti-modular (this is the uniqueness of type class instances). As a result, you can never add modularity to Haskell, but we may be able to back-port some of the more beloved aspects of Haskell to a new nephew in the ML family. (Confusingly, laziness advocates often say that their brand of functional programming has better "modularity" than strict, because of the way that you can compose lazy algorithms to get more lazy algorithms that don't totally blow up in complexity. I would say that lazy languages are more "compositional", not more "modular"—I prefer to use the latter term for modularity at the level of architecture and systems design, not algorithms.)

wyager 12y ago

>The most blatant violation is the all too necessary, but aptly named, unsafePerformIO The only time it's necessary is when you're using the FFI or working with language internals, at which point there's really no way for the type checker to work anyway. One should avoid using exceptions in pure code. This is well established. Instead, use any of the many type-safe exception mechanisms, like Maybe or Either. Having written probably in the high thousands or low tens of thousands of LoC of Haskell, I've never once used a user-defined exception or undefined. The point of this article seems to be "If your code breaks, it's no longer type safe.". I don't think this is news to anyone.

mercurial 12y ago
> Having written probably in the high thousands or low tens of thousands of LoC of Haskell, I've never once used a user-defined exception or undefined. Good for you, I guess. You'll find plenty of libraries which have no qualms about using exceptions in the real world, though. Not to mention asynchronous exceptions, obviously. Personally, I find both exceptions and type-safe error handling unsatisfactory. The former is unsafe, the latter results usually in a "god error type" which breaks modularity.
- wyager 12y ago
  >plenty of libraries which have no qualms about using exceptions in the real world I haven't run into too many (particularly when compared to the popularity of exceptions in other languages). >the latter results usually in a "god error type" which breaks modularity. Have you tried using Either with a sum error type and/or an error typeclass?
  - mercurial 12y ago
    > I haven't run into too many (particularly when compared to the popularity of exceptions in other languages). This doesn't mean much if you take a language like Java where it is the idiomatic way of handling errors. But take something vaguely complex like http-client (formerly http-conduit) and you get exceptions. > Have you tried using Either with a sum error type and/or an error typeclass? Well, even with sum types you get "god errors" which encapsulate all kinds of issues that can happen in your exception, because it's the path of least resistance. I haven't tried Either with a typeclass, though, but it sounds vaguely abusive.

tailrecursion 12y ago

I want to question the importance of soundness in type systems. Suppose you could catch 99% of type-based errors instead of 100%, and in addition, use a compiler switch to see all the case statements where a class of a type is missing. The intended benefit of this system is that it accepts all correct programs. Correct meaning, the program runs and returns the correct answer. Would such a language be viable? Or is it absolutely necessary to catch all possible type errors. In the past, tools like lint have been considered useful, although lint is not at all the kind of type system that I envision, namely a system that is in practice catching all the errors that ML catches -- it just doesn't (and cannot) guarantee it catches them. The restrictive nature of static type systems today is legendary, but I wonder sometimes whether people realize how restrictive they are. If you can't make your idea work with functors or typeclasses, chances are good there's no way to get it to compile and you have to write functions in longhand.

shadowfox 12y ago
There is always idea of Gradual Typing [1] which has been implemented with varying degrees of success. There are also a large set of static analysis theories/tools which can help here. It is also worth noting that if you dont want (global) type inference, you can get far in a language with permissive casting, type annotations and local inference. The results aren't a panacea though. > Suppose you could catch 99% of type-based errors instead of 100%, and in addition, use a compiler switch to see all the case statements where a class of a type is missing. I am not quite sure what you mean by this. Care to elaborate? (In general, with inference systems, missing type information is hard(ish) to localize. So pointing out where exactly a type error occurred is non-trivial) [1] https://en.wikipedia.org/wiki/Gradual_typing https://en.wikipedia.org/wiki/Gradual_typing
- tailrecursion 12y ago
  I'm thinking of a system with valueset inference where valuesets are not necessarily disjoint. So the system may infer that a return value is the disjunction {INTEGER | REAL}. In order to get precision in checking, a lot of computation needs to be done so the compiler relaxes the precision when facing large disjunctions (networks) of constraints. Dynamic checks are inserted as necessary but a system that relaxes when things get hairy can't guarantee that it will find all errors at compile time. The idea is similar to Soft Typing of Cartwright and others, but they were thinking of an interactive system, some kind of programmer's aid. If I recall they ran into problems giving reasonable error messages.

accessright 12y ago

So basically it is "unsafePerformIO" and "error" that is the problem? So if you do not use them (which I never do and it is recommended not to) then the problem is not relevant?

densh 12y ago
I think the main problem here is that it's not just you, but also your transitive dependencies.
Lambdanaut 12y ago
It seems to me that it would also be any function you import that uses these. Unfortunately, there are a lot of very commonly used functions that use `error`.

qwerta 12y ago

Being unsafe never stopped Ruby or PHP, while Ada is still nowhere.

CmonDev 12y ago
"never stopped Ruby or PHP" Lots of poorly-maintainable code is a good thing?
Horusiath 12y ago
Tell that next time you get on the plane.
progman 12y ago
http://www.ada2012.org http://www.ada2012.org
praptak 12y ago
This misses the point. Statically typed functional languages. Safety is the selling point here.

reirob 12y ago

Here the reddit thread about this article, from 2 years ago: http://www.reddit.com/r/haskell/comments/y74vn/robert_harper_haskell_is_exceptionally_unsafe/?already_submitted=true http://www.reddit.com/r/haskell/comments/y74vn/robert_harper...