3 ms·
Think original question I had, was if you make "f = undefined" be Pure. Don't leave undefined. It has a defined signature Int->Int. Then "f" should return Int
by FrustratedMonky 3y ago
Think original question I had, was if you make "f = undefined" be Pure. Don't leave undefined. It has a defined signature Int->Int. Then "f" should return Int every time guaranteed, and would be equivalent of the Total Functional case.
- lynx23 3y agoEven 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.