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
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)
-
-
Er, maybe the word "easily" doesn't belong in this tweet, sorry :)
0 replies 0 retweets 0 likesThanks. Twitter will use this to make your timeline better. UndoUndo
-
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.