Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Haskell Is Exceptionally Unsafe (2012)

existentialtype.wordpress.com

Post reply on HN
Print view View original

31–40 of 125 posts

Re: Haskell Is Exceptionally Unsafe (2012)

#31

Post by CmonDev »

jonsterling wrote: post #11

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 wi…

"the next great thing will be more like ML"

ocaML or even better F#?

Re: Haskell Is Exceptionally Unsafe (2012)

#33

Post by pjmlp »

coldtea wrote: post #30
pjmlp wrote: post #22

Earlier quoted context omitted.

Haskell belongs to the ML language family.

I'd bet that he knows that already. And C++ belongs to the C language family, but one could still say something like "the next great thing would come from a C rather than a C++ like language" (I'm not judging if this is true here, just that it's quite clear what it means).

No, because you can have other ML derived languages that are also lazy and strict, without being necessarily based on Haskell.

Re: Haskell Is Exceptionally Unsafe (2012)

#35

Post by tomp »

tailrecursion wrote: post #29
shadowfox wrote: post #21

Earlier quoted context omitted.

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 t…

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…

The problem with this idea, at least compared with current implementations of Haskell and OCaml, is that it requires runtime type information. Right now, Haskell and OCaml both perform erasure, and the only kind of runtime type information used is for the GC, but if you have two ADTs with identical structure (number of branches, payloads) but different names (i.e. they are different types), they will be encoded in the same way. So, in order to tell them apart, you would need some additional type information, which would require changes to compilers and would probably performance characteristics.

Re: Haskell Is Exceptionally Unsafe (2012)

#37

Post by millstone »

imanaccount247 wrote: post #23
tailrecursion wrote: post #19

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…

>I want to question the importance of soundness in type systems Why? The most common and popular opinion is already that it is not important. >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. That doesn't make sense. Tha…

Suppose we insisted in math that all proofs be computer-checkable. There would be no erroneous proofs, but there would also be many correct proofs that could not be accepted or even formulated. Mathematics would suffer overall.

Compiler enforced static typing rejects many correct programs, which is a disadvantage.

Re: Haskell Is Exceptionally Unsafe (2012)

#38

Post by lmm »

tailrecursion wrote: post #19

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…

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

It's entirely possible - I believe Dylan implements something on these lines. IMO it's harder to reason about than a consistent type system with "escape hatches" like unsafePerformIO, and about equivalent in usability.

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

I have yet to find a piece of "good code" that I couldn't implement in a typesafe way. I've occasionally found code that worked but couldn't be made typesafe (e.g. the "big global Map" antipattern), but it's always been code that I would have wanted to rewrite for readability and sanity anyway.

Re: Haskell Is Exceptionally Unsafe (2012)

#39

Post by berdario »

jonsterling wrote: post #11

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 wi…

Since there aren't a lot of full time Haskell developers, I'm curious to know what do you use to setup your projects and handle dependencies:

hsenv, cabal-dev, cabal sandboxes, nix, stackage ... or do you include everything in your repository (any tool to automate that)?

Re: Haskell Is Exceptionally Unsafe (2012)

#40

Post by thoughtpolice »

millstone wrote: post #37
imanaccount247 wrote: post #23

Earlier quoted context omitted.

>I want to question the importance of soundness in type systems Why? The most common and popular opinion is already that it is not important. >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. That doesn't make sense. Tha…

Suppose we insisted in math that all proofs be computer-checkable. There would be no erroneous proofs, but there would also be many correct proofs that could not be accepted or even formulated. Mathematics would suffer overall. Compiler enforced static typing rejects many correct programs, which is a disadvantage.

> Compiler enforced static typing rejects many correct programs, which is a disadvantage.

Only if you care about these programs. It is entirely possible many of these 'correct programs' are not useful at all, or arguably useful, or are outside the domain criteria, and rejecting them is fine. This is often a leading motivator behind the design of things like domain specific languages, or designs like MISRA C - many things by design cannot be done, but often those aren't the things we care about, use, or wish to discuss anyway.

On the flip side, there are things type systems enable that I do not think can be actually accomplished in an untyped language - but really, this isn't very interesting aside from being a minor technical factoid, IMO. It's very far removed from the more interesting question of whether or not it's useful to consider these things at all. And it's completely legitimate to say "No, these things aren't worth considering".

Post reply on HN