Live data from Hacker News

Haskell Is Exceptionally Unsafe (2012)

existentialtype.wordpress.com

91–100 of 125 posts

Re: Haskell Is Exceptionally Unsafe (2012)

#91

Earlier quoted context omitted.

Could you expand on why you think the next "great thing" will be more like ML than like Haskell?

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

> I think that Call-by-push-value can help us with both recovering the benefits of laziness as well as reasoning about effects.

I would be very interested to hear why you think that, or just have some links on the subject. In particular it's not clear to me how CBPV helps us reason about effects.

Re: Haskell Is Exceptionally Unsafe (2012)

#92
post #91

Earlier quoted context omitted.

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

> I think that Call-by-push-value can help us with both recovering the benefits of laziness as well as reasoning about effects. I would be very interested to hear why you think that, or just have some links on the subject. In particular it's not clear to me how CBPV helps us reason about effects.

It might help to read Levy's thesis, which is source on CBPV. Also read the literature on Conor McBride's Frank, which is based on a variant of CBPV.

Re: Haskell Is Exceptionally Unsafe (2012)

#93
post #88

Earlier quoted context omitted.

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

The best argument for John's thesis is the proliferation of ML derivatives in industry: Swift, Rust and Facebook's Hack. I'm really looking to Facebook's Flow which adds an ML style type system to Javascript.

I would be very cautious about saying "popularity" or "proliferation" suggest that something is good. The ML family happens to have proliferated very nicely, but this is not why it is good.

Re: Haskell Is Exceptionally Unsafe (2012)

#94
post #87

Earlier quoted context omitted.

I'm learning F# right now, it's flipping excellent! From what I understand it's similar to Ocaml, but has some other features that give it the edge (for me at least). I did try to learn Ocaml at one point, but I was put off by the standard library variation (the default one apparently has numerous shortcomings, Batteries project extends it and Core project aims to replace it, but neither one is the clear winner) and…

Thanks a lot for these infos! Unfortunately F# is .NET only. Linux requires Mono for installation which means a lot of dependencies. I prefer small efficient solutions (Nimrod for instance). OCaml works out of the box on my system.

Rare language has both .Net and JVM support, probably only Clojure now. On the upside you can build iOS and Android apps using F# plus many other gaming platforms.

Re: Haskell Is Exceptionally Unsafe (2012)

#95
post #70

Earlier quoted context omitted.

Could you expand on effects which preserve extensionality some more? I'm fairly sure I understand it, but I've never quite follows what Harper's "benign effects" meant in detail and I'd like to see how it all connects.

The most benign effect of them all is laziness. Haskell uses this in lieu of all other effects, basically. So memoizing data structures, or a higher order function for memoizing, utilizes a "benign effect".

So extensionally equal simply means that there is a model with and without the effect such that extensionally, according to some model of observation, we cannot discern the existence of the effect?

So, laziness is benign in total fragments.

Re: Haskell Is Exceptionally Unsafe (2012)

#96
post #81
post #71

Earlier quoted context omitted.

I would love to see a "practical" CBPV language.

Likewise, mostly because it would probably help me understand what CBPV actually is!

It's remarkably easy to understand if you're already used to monads. Levy's thesis is a bit opaque from that POV, but not unpleasant to read.

Re: Haskell Is Exceptionally Unsafe (2012)

#97
post #53

Earlier quoted context omitted.

Why not? I'd say that Agda/Idris/Coq are substantially the same languages with variation arising only in the kind of styles of coding they emphasize.

But isn't this a variant on the old "but it's Turing-complete, therefore you can do anything" fallacy? Sure, their type system may be similar, but the question is, which one will let you write, say, a robust, maintainable HTTP client with the least amount of pain?

I suppose that's true. I guess in my eyes DTs are such a meteoric difference that Idris is not sufficiently more interesting than the others yet. But time will tell if they manage to build a better way to manage proofs, for instance, they could really change the game.

Re: Haskell Is Exceptionally Unsafe (2012)

#98
post #52

Earlier quoted context omitted.

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…

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.

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.

Re: Haskell Is Exceptionally Unsafe (2012)

#99
post #95

Earlier quoted context omitted.

The most benign effect of them all is laziness. Haskell uses this in lieu of all other effects, basically. So memoizing data structures, or a higher order function for memoizing, utilizes a "benign effect".

So extensionally equal simply means that there is a model with and without the effect such that extensionally, according to some model of observation, we cannot discern the existence of the effect? So, laziness is benign in total fragments.

I wasn't thinking about models, but perhaps you could? I just mean that you get the same results for equal inputs; laziness is fine in this respect (but not in the presence of some other effects).

Re: Haskell Is Exceptionally Unsafe (2012)

#100
post #96
post #81

Earlier quoted context omitted.

Likewise, mostly because it would probably help me understand what CBPV actually is!

It's remarkably easy to understand if you're already used to monads. Levy's thesis is a bit opaque from that POV, but not unpleasant to read.

Hmm, really? I just read a couple of papers linked from his website, but I'm still not feeling enlightened.
Post reply on HN