3 ms·

> 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

• 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.