Comment by lexi-lambda
6 years ago
> But the type itself doesn't say that it must return the first element.
Sure, I didn’t say it does. That type isn’t a full specification of head. This blog post isn’t about proving literally everything in your program correct, which is impractical anyway because if you did that it would be as easy to prove the wrong thing as to write a bug in the first place. Some functional tests are still needed.
> Okay, what about more complex cases? E.g. how do you describe type "such value doesn't exist in the db table yet"?
I’ve addressed that kind of question more generally in another comment[1], but for that specific case, I think it probably isn’t worth proving, because a database lives outside of your application, and it’s the database’s responsibility to manage that kind of data integrity, not your application logic. That’s one of the kinds of “execution-phase failure modes” that I describe in this paragraph of the blog post:
> Parsing avoids this problem by stratifying the program into two phases—parsing and execution—where failure due to invalid input can only happen in the first phase. The set of remaining failure modes during execution is minimal by comparison, and they can be handled with the tender care they require.
> Sure, I didn’t say it does.
Sorry, I implied it from your "foo" example.
> two phases
So maybe we need to change the mantra to “parse, and validate as little as possible”?