[Haskell-cafe] Pattern matching, and bugs

[wren ng thornton]

Ketil Malde wrote:
> András Mocsáry <amocsy at gmail.com> 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