2 ms·
No. Haskell has this notion of what they call "bottom", more easily remembered as what happens if you call undefined. The issue is, your function can be as pu
by lynx23 3y ago
No. Haskell has this notion of what they call "bottom", more easily remembered as what happens if you call undefined. The issue is, your function can be as pure as it wants, as long as you are able to write "f :: T -> T; f = undefined" all your purity based analysis goes to hell.
- FrustratedMonky 3y agoThink 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.
- justincredible 3y ago[dead]