On 05/07/18 08:28, PY wrote:
Hello, Cafe!
There is an opinion that Bool type has problems. It's "dangerous", because it's not good to be used as flag for success/fail result. I read this post: https://existentialtype.wordpress.com/2011/03/15/boolean-blindness/ and was shocked. How popular is such opinion? Is it true, that bool is "bad" type?
The text never uses the word "dangerous" or "bad", it says that the Bool type is boring, carries no information and leads to blindness. For instance, let's say that you want to call `head` on a list. But `head` is a partial function, so you need to check first if the list is not empty. Then you branch on the result of the test and call `head` or do something else in the other branch. At first the code is clear and easy to follow. But after several refactorings and new features, the call to `head` was pushed far away from the emptiness test. As you can see, this code is now very fragile. If someone changes the test to something else it will still compile but `head` may now fail at run time. On the other hand, if you use a type expressive enough to encode a proof that the list is not empty (trivial in Agda or Idris), that proof will be in scope and a total version of `head` will only compile if it finds the proof. Cheers, -- -alex https://unendli.ch/