> I still haven't fully grasped what aspect of Haskell means you can't rigorously reason about your code.
Oh, that particular criticism wasn't aimed at Haskell, but rather at languages without compound values. And I never said you can't reason rigorously about code written in such languages. You can, but it isn't very pleasant.
> I'm pretty sure you don't mean global coherence of type classes, which are the two most popular complaints about reasoning about Haskell.
Far more serious one: Haskell doesn't have a type whose value inhabitants are the integers and nothing else. I would like to say “even Lisp has that”, but nope, it doesn't either: https://news.ycombinator.com/item?id=12328095
> Sure, I get that, but I don't get the practical consequences for reasoning.
(0) In a language without compound values, you need to manually prove that object states faithfully represent the compound values you care about.
(1) In a dynamically typed language, you need to manually prove that computations produce the classes of values that their continuations expect.
(2) In a lazy language, you need to manually prove that variables will never be substituted with nonterminating computations.
> What's an example of something you wanted to prove in Haskell but couldn't, because it wasn't strict?
All the usual type class laws, without the pesky addendum “assuming no free variables are ever substituted with bottom, globally”. (In all fairness, strictness alone doesn't fix the problem either. At least not when laws have free variables of function type.) Redefining what variables can be substituted with is redefining the language's operational semantics, which in turn is effectively creating a new programming language. You would have to prove all the usual things from scratch: that type checking is decidable, that the type system is sound, etc.
In practice, I can still prove the things I want, but the proofs themselves are less modular in a lazy language. The problem manifests itself when you build large computations from smaller ones:
(0) In a strict language, whether any of the subcomputations terminates is a local issue, and doesn't affect the other subcomputations.
(1) In a lazy language, failure of one computation to be productive may be observed as a termination problem in a different computation.
Oh, that particular criticism wasn't aimed at Haskell, but rather at languages without compound values. And I never said you can't reason rigorously about code written in such languages. You can, but it isn't very pleasant.
> I'm pretty sure you don't mean global coherence of type classes, which are the two most popular complaints about reasoning about Haskell.
Far more serious one: Haskell doesn't have a type whose value inhabitants are the integers and nothing else. I would like to say “even Lisp has that”, but nope, it doesn't either: https://news.ycombinator.com/item?id=12328095