4 ms·

> 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

> 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 9y ago
> 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 9y ago
  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.

dllthomas 9y ago

> 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 9y ago
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.