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'
_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
