compilation of pattern-matching?

[Lennart Augustsson]

Sorting by constructor tag is perfectly safe when done right.
You can read about how to do it in my 1985 FPCA paper or in Simon's book.

When pattern matching against against things that that are not
constructors (like literals etc) it's much trickier to reorder them
since you have to prove harder pattern commutation properties.

I don't think there is any controversy at all about Haskell pattern
matching semantics.
As you say, it's pretty clearly spelled out.
(It wouldn't hurt to have it written down as a denotational semantics, though.)

And ghc happens to have a bug.

  -- Lennart

On Fri, Mar 27, 2009 at 12:10 AM, Claus Reinke <claus.reinke at talk21.com> wrote:
>> So a first comment on this.  I spoke too soon, ghc clearly has a bug here.
>> It shouldn't reorder those matches against literals like that.
>> I suggest you report that bug, because, as you say, it violates the H98
>> report.
>
> It would be nice if we could first reach a common understanding, so
> that I can actually report the right problem, not just isolated symptoms.
>
>> But I don't think that bug at all affects the function you had in your
>> original email.
>
> The argument goes like this:
>
> - Haskell does prescribe the order in which patterns are matched
> - Haskell does permit alternative implementations if they respect
>   certain equations; in other words, there is a proof obligation
>   associated with things like reordering patterns
> - for types like 'data AB = A | B', we know that a successful match
>   for 'A' implies a failing match for 'B', and vice-versa
> - disregarding performance (which the language definition does
>   not talk about), we therefore know that in 'case e of A->a;B->b',
>   we don't need to match for both 'A' and 'B'; instead, we can   either
> match for 'A' and enter 'a' on success and 'b' on failure,
>   or match for 'B' and enter 'b' on success and 'a' on failure
> - another view of this is that 'not isB' is actually the same as 'isA',
>   so we're matching for both in one test
> - so, if we want to, we can fulfill the proof obligation involved   with
> reordering the patterns, or we can argue that by matching
>   for 'B', we are actually matching for 'A' as well
>
> So far, we have:
>
> - pattern order does matter, by language definition
> - GHC can nevertheless reorder patterns where it can prove   that this isn't
> observable
>
> You are right that this doesn't help my performance argument,
> as performance issues are outside the language definition (not
> observable in the language definition sense). It was merely an answer to the
> vehement claims that pattern order is irrelevant.
>
> And it has practical implications, too: the proof obligations are
> getting harder to fulfill as pattern-match expressiveness improves.
>
> For Haskell'98, we can't reorder: guards, overlapping patterns,
> numeric literals, (others?). For GHC Haskell, we also can't reorder: view
> patterns, string literals (IsString/fromString), quasiquotes?, .. . And the
> list keeps growing, as DSL authors want IsBool/fromBool, container-library
> authors want IsList/fromList, etc.
> In other words, this
>
> |It's not that GHC deliberately re-orders case alternatives, |it's that it
> doesn't deliberately not do it.
>
> no longer is a safe default strategy (actually, it never was, as
> the bug shows;-). Neither is sorting patterns by constructor tag,
> as seems to happen on the way to Core.
>
> GHC needs to consider every individual case before being lax about pattern
> order, and the result of that consideration might change over time: in
> Haskell'98, []/: patterns can be reordered for [a], in GHC Haskell, []/:.
> patterns can be reordered for [a], as long as a/=Char, in GHC Haskell with
> an IsList class, []/: patterns can not be reordered in general.
>
> This is independent of performance considerations, just a
> consequence of the language definition, and our abilities to
> observe deviations from the prescribed sequential order.
>
> Claus
>