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

21–30 of 125 posts

Re: Haskell Is Exceptionally Unsafe (2012)

#21

Post by shadowfox »

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…

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

Re: Haskell Is Exceptionally Unsafe (2012)

#22

Post by pjmlp »

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…

Haskell belongs to the ML language family.

Re: Haskell Is Exceptionally Unsafe (2012)

#23

Post by imanaccount247 »

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. That's like saying suppose we had a system of math that gave the right answer 99% of the time. How would doing the wrong thing 1% of the time give you the benefit of accepting all correct programs?

>The restrictive nature of static type systems today is legendary

Mythological. Legends are supposed to have some historical root.

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

What does that even mean? That's like saying "if you can't make your idea work with classes or inheritance, chances are good that there's no way to get it to compile and you have to write functions in longhand".

Re: Haskell Is Exceptionally Unsafe (2012)

#24

Post by mercurial »

Chinjut wrote: post #7
eagle2001 wrote: post #6

Earlier quoted context omitted.

"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." Examples, please. (I like bright, shiny things.)

Perhaps Coq, Agda, Idris, and other such dependently-typed languages are to be considered, at least in some dimensions, "more advanced" than Haskell.

I wouldn't say full-blown theorem provers (Coq, Agda) are really in the same category as Idris, which is supposed to be more practical.

Re: Haskell Is Exceptionally Unsafe (2012)

#25

Post by lumpypua »

coolsunglasses wrote: post #15
lumpypua wrote: post #10

Earlier quoted context omitted.

As an intermediate Haskeller I'm curious, what's the replacement for SYB? I've worked in haskell primarily on compiler-like tree tranformation code and SYB seems to fit the bill perfectly.

The direct equivalent and replacement is GHC http://www.haskell.org/haskellwiki/Generics . Edit: I just wanted to add that if you do compiler-like tree transformation code it behooves you to explore uniplate/multiplate/plated.

Sick, thank you for the reply and pointer to uniplate and associated tools!

Re: Haskell Is Exceptionally Unsafe (2012)

#26

Post by mercurial »

wyager wrote: post #14

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

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

Re: Haskell Is Exceptionally Unsafe (2012)

#29

Post by tailrecursion »

shadowfox wrote: post #21
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…

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

Re: Haskell Is Exceptionally Unsafe (2012)

#30

Post by coldtea »

pjmlp wrote: post #22
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…

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

Post reply on HN