4 ms·
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. O
by catnaroek 10y ago
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 http://www.cs.bham.ac.uk/~pbl/cbpv.html. The danger is that they might want to switch to a strict language.
- danharaj 10y agoHaskell* is essentially an extension of System F. System F has no set models. * Need to enable a few extensions.
- catnaroek 10y agoOh, 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?
- dllthomas 10y ago> 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.
- tome 10y agoI 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.