Even if undefined were not allowed, you'd still be able to write "f :: Int -> Int; f x = f x" which would never return an Int. Totality is about getting a grip

Even if undefined were not allowed, you'd still be able to write "f :: Int -> Int; f x = f x" which would never return an Int. Totality is about getting a grip on these cases. As mentioned more elquently then I could in this thread, it has been proven long time ago that termination-analysis is impossible to achieve. What Idris for instance does is to use proofs, adn to an extend heuristcs, to stil decide in special cases that a function is total, IOW terminates. Thats a pretty cool part of CS, since we're basically knowing something is impossible but still make small steps towards tackling the issue at least for some cases we care about.