> As far as I've heard, Haskell's type system doesn't normally prove functions to be total; they can diverge. This is true. You can write a function which is

> As far as I've heard, Haskell's type system doesn't normally prove functions to be total; they can diverge. This is true. You can write a function which is the natural numbers, and I wouldn't want the type system to preclude it. nats :: [Integer] nats = [1..] However, I would love to be able to opt in to declaring functions total on a case-by-case basis, like Idris can. > This fine, though, because for ordinary programming, a proof of totality isn't a useful guarantee. You care how long programs actually take to run, not whether they would theoretically finish eventually. This wouldn't be the point of the guarantee for me. Haskell functions already give you assurances that you've not made any mistakes: * You haven't accidentally introduced null, or missed any null checks. * You haven't written code which will do a different thing tomorrow than it did today. * Your function won't race, nor will it cause other functions to race. If you have a function Foo->Bar, and you give it a Foo, you've all-but-proved that you'll get a valid Bar back. How can you screw that up? By diverging. I'm not trying to put a bound on a long-running function, I just want the type system to make sure the function isn't sucking on its own tailpipe.