Hacker News Reader

Comment by catnaroek | Hacker News Reader

It's been known for quite a while that Haskellers live in a make-believe world where totality is taken for granted, and Hask is morally the category of sets.

One possible fix is to read the call-by-push-value papers: http://www.cs.bham.ac.uk/~pbl/cbpv.html. The danger is that they might want to switch to a strict language.

View on HN

I am one of the foremost proponents of Haskell on HN, and you know what? I actually agree with you that a strict language with explict thunk data type would likely be a better way to program. But your attitude really discourages your potential allies from constructively engaging with you.

> It's been known for quite a while that Haskellers live in a make-believe world

Or some of us live in the real world where we get work done with useful but imperfect tools, and are pretty aware of where our abstractions run risk of breaking down in practice.

Haskell* is essentially an extension of System F. System F has no set models.

* Need to enable a few extensions.

Oh, that's another thing that makes me really angry too: GHC's lack of distinction between first-class polymorphism (functions from types to values, à la System F(ω)) and second-class polymorphism (values, not necessarily functions, that admit more than one type, à la Damas-Milner). But that's a topic for another day.

EDIT: Also, I forgot, I haven't actually seen Haskellers use ImpredicativeTypes much. Are you really sure that the predicative subset of System F (just RankN types) has no set models?

Reply on news.ycombinator.com