There's a common belief floating around that total functions are an essential component of functional programming. I suppose there's growing demand for developing in Turing-incomplete languages.
-
-
Replying to @eiriktsarpalis
a nice paper of David Turner about this: http://www.jucs.org/jucs_10_7/total_functional_programming … Anyway I'm pretty ok with
@edwinbrady pacman completeness1 reply 0 retweets 3 likes -
Replying to @giacomociti @edwinbrady
Don't get me wrong, reasoning about totality is useful. Total functions are however not a defining characteristic of FP, as is often erroneously claimed on twitter.
1 reply 0 retweets 0 likes -
Replying to @eiriktsarpalis @edwinbrady
I don't have a strong opinion on this, but those who claim that programming is math (I like theory but I'm not in this camp) tend to forget that totality is at odd with Turing completeness
2 replies 0 retweets 0 likes -
Replying to @giacomociti @eiriktsarpalis
It isn't, though... https://www.google.co.uk/url?sa=t&source=web&rct=j&url=https://pdfs.semanticscholar.org/e291/5b546b9039a8cf8f28e0b814f6502630239f.pdf&ved=2ahUKEwihiZzT-rvaAhWDZFAKHYd8A44QFjAAegQIBxAB&usg=AOvVaw3pR02o1ah-4Wqnmhyk2BKW … (Not to say it's easy, but that when we've made total programming easier the price is not that we lose Turing completeness)
1 reply 0 retweets 1 like -
Replying to @edwinbrady @giacomociti
Thanks for sharing. I’ve attended your talk on total prgramming in Idris and it was very interesting. But it seems those type systems are capable of proving totality for special cases of well-founded recursion? There are total recursive functions outside that classification.
1 reply 0 retweets 0 likes -
Replying to @eiriktsarpalis @giacomociti
Of course, there'll always be things you can't decide. The challenge is to learn how to spot more of them. But even within current constraints, you can still have Turing completeness.
2 replies 0 retweets 0 likes -
Replying to @edwinbrady @giacomociti
Buchberger’s algorithm jumps to mind. We know that it terminates, however this assumes a weak version of AC. Is there a way in Idris to declare a function to be total even if the type checker cannot prove this, an unsafePerformIO for total functions?
1 reply 0 retweets 1 like
You can assert totality, at least.
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.