4 ms·
Total functional programming indeed is another example of a valid approach to weakening cycles and thereby guaranteeing termination. Although it works for that,
by jondgoodwin 6y ago
Total functional programming indeed is another example of a valid approach to weakening cycles and thereby guaranteeing termination. Although it works for that, it is too restrictive for my taste. I am looking for less restrictive forms of weakening that allow creation of a broader range of algorithms (including "imperative") that we can still guarantee will terminate.
- lmm 6y ago> Although it works for that, it is too restrictive for my taste. I am looking for less restrictive forms of weakening that allow creation of a broader range of algorithms (including "imperative") that we can still guarantee will terminate. How is it weak? Surely it's equivalent to any other approach: given a function and any form of termination guarantee for that function, you can encode that guarantee as a phantom type and then you have an expression of that function in a total functional language.
- remexre 6y agoI mean, how long does it take to convince yourself a function will halt vs how long does it take to use implement it with well-founded recursion, with comparable readability? Not that it's not possible, it's just more of a pain.