
Ketil Malde wrote:
András Mocsáry
writes: Now we have a problem, which is most generally fixed in these ways: C-like:
switch ( x ) { Case 0: "Unchecked" Case 1: "Checked" Case 2: "Unknown" Default: "Nothing" }
This is not a fix, this is a workaround for a design bug, namely that x is of a type that allows meaningless data.
Indeed. In C-like languages it is common practice to use integers to mean just about anything. Often there are fewer of "anything" than there are integers, and so hacks like this are necessary to work around the ensuing problems. But ultimately, this is a *type error*. The proper response, in Haskell, to type errors like this is not to add hacks catching bad values, but rather to change the types so that bad values cannot be constructed. As a few others have mentioned, rather than using an integer, you should define a new type like: data X = Unchecked | Checked | Unknown and then require that x is of type X. Thus the pattern-checker can verify that all possible values of x will match some case option. The reason Haskell (or other typed functional languages) allow proving correctness so much easier than other languages is because we create new types which correctly and precisely match the set of values we want to belong to that type[1]. By pushing as much of the correctness logic as possible up into the type layer, this frees us from needing to check things at the term layer since the type-checker can capture type errors automatically. But it can't catch things we haven't told it are errors. [1] For some complex sets of values this isn't possible with Haskell's type system, which is one of the reasons for the recent interest in dependently typed languages. However, for most familiar sets of values (and quite a few unfamiliar ones) Haskell's type system is more than enough. -- Live well, ~wren