Typing should be a conversation with the compiler. If you have a strong understanding of what you are writing then, yes, writing the types first makes sense. On the other hand, sometimes I only understand how some particular pieces fit together—at this point, I want the compiler to throw its inference engine at my code fragment and tell me everything it can!
Typing and programming is exactly the same as theorem stating and proving in mathematics. It would be idiotic to have one-way information flow only.
That said, it's also practically criminal to just hand someone a proof without stating what you think it's supposed to be proving. Ultimately, that it where you must wind up.
Not at all!
Typing should be a conversation with the compiler. If you have a strong understanding of what you are writing then, yes, writing the types first makes sense. On the other hand, sometimes I only understand how some particular pieces fit together—at this point, I want the compiler to throw its inference engine at my code fragment and tell me everything it can!
Typing and programming is exactly the same as theorem stating and proving in mathematics. It would be idiotic to have one-way information flow only.
That said, it's also practically criminal to just hand someone a proof without stating what you think it's supposed to be proving. Ultimately, that it where you must wind up.