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 completeness
-
-
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
But presumably TC is only attainable once you invoke the general recursion effect, where reasoning about termination is forsaken, as far as the type checker is concerned.
1 reply 0 retweets 0 likes -
Replying to @eiriktsarpalis @giacomociti
The idea is that you can describe general recursion, or partiality, in much the same way as you can describe interactive programs.
1 reply 0 retweets 0 likes -
Running general recursive programs requires a (very small) driver, but I don't consider this an issue because so does evaluation and execution in general.
1 reply 0 retweets 0 likes -
And one could easily imagine a total, turing complete language, where such a driver is part of the run time system in the same way as a driver for executing effects (like Idris/Haskell have)
1 reply 0 retweets 0 likes
Er, maybe the word "easily" doesn't belong in this tweet, sorry :)
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.