Avdi is a great developer who I have learned a lot from, but I think he is exactly wrong here. A thread.https://twitter.com/avdi/status/1114181834353647616 …
-
Show this thread
-
A syntax error is an error, and errors should be raised at runtime. Therefore, syntax errors should be raised at runtime. This follows from Avdi's argument.
2 replies 0 retweets 17 likesShow this thread -
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.
1 reply 1 retweet 40 likesShow 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
Me too :). But it's okay to write simply typed programs in a dependently typed language. My recent experience has been that it's worth spending time getting your core types right and seeing where that takes you.
-
-
Also holes. Leave holes, see where the runtime errors end up needing to evaluate the holes, and learn more about the domain as a result. Statically typed languages need holes to be a first class construct.
0 replies 0 retweets 7 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.