Comment by privethedge
6 years ago
> head :: [a] -> a
> This function returns the first element from a list. Is it possible to implement?
But the type itself doesn't say that it must return the first element.
> If you see why parseNonEmpty is preferable, you understand what I mean by the mantra “parse, don’t validate.”
Okay, what about more complex cases? E.g. how do you describe type "such value doesn't exist in the db table yet"?
> 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.
[1]: https://news.ycombinator.com/item?id=21478427
> 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”?
> Okay, what about more complex cases? E.g. how do you describe type "such value doesn't exist in the db table yet"?
If that's supposed to be an error state then you just throw a different error.
If it's not supposed to be an error state, then you can have something like a function that accepts a type of "Input" and returns a type of "DBTrackedInput" and in that function you do your saving to the DB. Then things which only want to work with values that are in the DB accept types of DBTrackedInput. That prevents you from passing something which hasn't been saved in the DB to those functions.
And you can expand from there, maybe the function that saves to the DB only accepts input of type "ValidatedInput". So you first have a function that accepts an "Input", validates it, and emits a "ValidatedInput". Then you have other functions, like your DB saver, which can say "I only want validated data" and still other functions which can say "I only want data that's been saved to the DB".
What if there is another application (or e.g. a stored procedure) that uses this DB table so you cannot control all saving operations from your application?
Don't do that. A DB table is too big and complex a surface to use as an interface between multiple applications. Each table should have one clear owner; if multiple components need to access the same table, put it behind a service rather than having them access it directly.
> how do you describe type "such value doesn't exist in the db table yet"?
Depends what you mean by that, but depending on the context, you may not want this in a type.
If it's a "Dirty" value / not inserted yet, you can just wrap it with "newtype Dirty ... = SomeRecordType ...".
If you mean something that you just checked that isn't in the database, you probably just want a properly named true/false, or a Maybe result. Encoding the value itself as not existing in the database will just bite you when something else inserts one in the meantime.
> But the type itself doesn't say that it must return the first element.
The "-> a" means a guarantee you will always get an "a" (by definition). This is why the fix is to change the return type to "Maybe a" which includes "Nothing". Why it isn't like that by default in Haskell is a different issue, but the return type is really guaranteeing that "a".