H98 Report: semantics of pattern matching

[Ross Paterson]

In section 3.17 Pattern Matching, there are some inconsistencies between
the informal and formal semantics:

(1) Section 3.17.2 Informal Semantics of Pattern Matching needs an extra
rule (before rule 2):

	Matching _|_ against the pattern con pat, where con is a
	constructor defined by newtype, is equivalent to matching _|_
	against the pattern pat.

(2) Rule 3 "Matching _|_ against a refutable pattern always diverges" is
untrue, because rules 4(b) and (c) (numeric literals and n+k patterns)
are also applicable to _|_, and it is possible to define the Eq, Ord
and Num classes so that pattern matching is non-strict:

> data Foo = Foo
> instance Eq Foo where _ == _ = True
> instance Ord Foo where _ > _ = False
> instance Show Foo
> instance Num Foo

> f :: Foo -> Int
> f 0 = 20

> g :: Foo -> Int
> g (n+1) = 20		-- Hugs incorrectly requires the Integral class

so f undefined = g undefined = 20.  Other definitions could be hyperstrict,
so _|_/non-_|_ distinction isn't relevant.

I'd suggest changing rule 3 to

	Matching _|_ against a pattern whose outermost component is a
	constructor defined by data always diverges.

deleting rule 4 and promoting the subrules, removing "non-_|_" from (c)
and changing "if x < k" to "otherwise".  You might wish to say it diverges
if x >= k does, but maybe that's too formal.

(3) Section 3.17.3 Formal Semantics of Pattern Matching needs an extra
equation:

	case _|_ of { K x1 ... xn -> e; _ -> e' } = _|_
	where K is a data constructor of arity n

(4) Equation (r) uses let, suggesting the possibility of polymorphism --
I'd suggest changing the rhs to

	if v >= k then case v-k of { x -> e } else e'