I frequently see the sentiment among FP programmers that they'd like to have a language where partial functions didn't compile. I don't think you'd want to use such a language (just yet). Thread with lots of subjective opinions:
-
Show this thread
-
The goal is of course noble: avoid more runtime errors. So, to be clear: this is not a dunk on people who'd like to have such a language. Idris, for example, can do that. By default, partial functions don't compile.
2 replies 0 retweets 4 likesShow this thread -
But: partiality comes from various things. Not only incomplete matches, but also non-termination. Now, as opposed to incomplete matches, termination is an undecidable problem!
5 replies 0 retweets 12 likesShow this thread -
What we would want is a language that has good termination checking built in. However, I don't think we (as in "research") are there yet. In practice, functions get complicated, you'll have to do a manual termination proof.
1 reply 0 retweets 8 likesShow this thread -
Case in point: recursive parser combinators are notoriously difficult in that respect. You'll have to distinguish (probably in the type) if a parser consumes at least one token or not in order to have a viable termination measure.
2 replies 0 retweets 7 likesShow this thread -
That REST library you were going to write? Have fun spending 80% of your time on termination proofs.
1 reply 1 retweet 16 likesShow this thread -
An alternative would be to track potential non-termination in the type, just like IO that tracks effects in the type. But that also has its downsides, as such "omnibus" types tend to be viral.
2 replies 0 retweets 4 likesShow this thread -
(One thing that I didn't mention is the dual of termination: productivity. Proving productivity for nontrivial corecursive functions is even harder. Automatic proofs are computationally expensive.)
1 reply 0 retweets 7 likesShow this thread -
In conclusion: applying full totality checks in real world languages on real world problems is very hard and requires loads of more research to make it ergonomic.
4 replies 1 retweet 14 likesShow this thread
Just as a nitpick (sorry!) Idris does compile partial functions by default, but it won't reduce them while typechecking. Otherwise I largely agree with this. I find pattern coverage checking extremely valuable though, and easier to achieve with dependent types.
-
-
Replying to @edwinbrady
Yes, thanks for the correction. But the sentiment I hear frequently isn't "we want warnings for incomplete patterns" (fair) but "we don't want to compile partial functions".
1 reply 0 retweets 0 likes -
Replying to @larsr_h @edwinbrady
My complaint is that you need ghc -Wall to get the incompleteness warnings
1 reply 0 retweets 0 likes - 1 more reply
New conversation -
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.