[evincarofautumn]

> developers who cannot restrain themselves

That’s pretty much all of us IMO. We need to get stuff done, and if there’s a feature available that lets us do it quicklier, we use it. We take the path of least resistance—a warning saying “don’t” provides no actual resistance.

That’s why I like languages like Haskell that by default prevent me from doing anything I’m probably going to regret later; if I want to break referential transparency, type safety, memory safety, &c. then I can always opt in explicitly and grep for it later when it hits the fan.

That said, I do prefer C over C++—really, the only things I miss are destructors (local automatic memory management is nice) and templates (generic/type-level programming is nice), but they’re not critical for the kinds of stuff I use C for anyway.

[dllthomas]

> That’s why I like languages like Haskell that by default prevent me from doing anything I’m probably going to regret later

    head []

(Not that I disagree with what you want, just that even Haskell has made some mistakes :-P)

[evincarofautumn]

Nah, that’s fair. However, here’s a neat trick—look at the type of “head”:

    ∀a. [a] → a

Viewed as a logical formula, it’s not a tautology, so I know it must be partial. Proof:

    Given: L(a) = μr. 1 + (a × r)

    ∀a. L(a) → a
    = [definition of L]
    ∀a. (μr. 1 + (a × r)) → a
    = [unroll μ]
    ∀a. (1 + (a × μr. 1 + (a × r))) → a
    = [∀xyz. (x + y) → z ⇔ (x → z) × (y → z)]
    ∀a. (1 → a) × ((a × μr. 1 + (a × r)) → a)
    = [(∀a. 1 → a) = 0]
    ∀a. 0 × ((a × μr. 1 + (a × r)) → a)
    = [∀x. 0 × x = 0]
    ∀a. 0
    =
    0

Unfortunately, this is also false if a is false (void/bottom), and all those “→ a”s are actually “→ ¬¬a” because Haskell isn’t a total language—with that pesky intuitionistic double-negative, any function can be partial. But it’s a good rule of thumb for quickly checking whether a function must not return for some (or all) inputs.