The alternative is to acknowledge that some errors should be raised at runtime and some should be raised at compile-time. Now we're just haggling about which ones.
-
Show this thread
-
So you might ask: why is checking syntax at compile-time good? It's good because a file with a syntax error is not even a program, and there's no sense in trying to run it at all. This exact argument applies to type errors.
3 replies 6 retweets 59 likesShow this thread -
Replying to @ReinH
Not quite. Rice’s theorem implies typecheckers will reject programs that have no runtime errors. Not the case for syntax errors.
1 reply 0 retweets 2 likes -
Replying to @Blaisorblade @ReinH
Viceversa, you *can* eliminate all runtime errors via types (through correctness proofs), but usually the extra benefits are too expensive. What’s the tradeoff?
2 replies 0 retweets 1 like -
Replying to @Blaisorblade
These things are of course true, but my argument is about pragmatics.
3 replies 0 retweets 1 like -
Replying to @ReinH
I’m also biased by having failed for months to write programs with dependent types that are trivial with normal types. Pragmatically, the amount of typing in ML/Haskell is probably a sweet spot, but I’m not sure how much is the extra cost for type-safe meta programming for most.
2 replies 0 retweets 2 likes -
Replying to @Blaisorblade
I am hopeful that with what we learn from
@edwinbrady's Idris, we will be able to build a new programming language that will show us where the sweet spot REALLY is.2 replies 0 retweets 2 likes -
Replying to @ReinH @edwinbrady
More like, this might move the sweet spot. At the very least, Edwin is trying to bootstrap Idris. Which most other systems aren’t remotely trying. (In part, that might be because of technological choices.)
2 replies 0 retweets 1 like -
Replying to @Blaisorblade @edwinbrady
(I am not trying to say anything bad about Idris, to be clear. I am very fond of it.)
1 reply 0 retweets 0 likes -
I think Idris is the prototype of even better languages to come.
1 reply 0 retweets 2 likes
I have plenty of bad things to say about Idris :). Most of them because we have to do something badly before we have any hope of doing it well. Best to pay attention to what didn't work while we're at it.
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.