[Haskell-cafe] Bool is not...safe?!

[Alex Silva]

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/