Match guards

From Successor ML

Contents 1 Introduction 2 Motivation and Example 3 Assumptions 4 Syntax 5 Static Semantics 6 Dynamic Semantics 7 Interactions 8 Compatibility 9 Implementation

Introduction

We propose adding conditional matches.

Motivation and Example

Match guards avoid code duplication by letting pattern matching fall through if a particular condition is not met. This is not possible by merely using conditionals on the right-hand side.

TODO: good example.

Assumptions

None.

Syntax

Defined by the following modifications to the Definition:

• In Appendix B, Figure 20, change the production for mrule as follows:

   mrule ::= pat <if exp> => exp

• In Appendix B, Figure 21, extend the production for fvalbind by adding

   <if atexp_i>

(with i = 1..m) to each equation, as the last component of the left-hand side.

• In Appendix A, Figure 15, add the following box:

   Matches match
   +---------------------------------+--------------------------------------------------+
   | pat if exp_1 => exp_2 <| match> | vid => case vid of pat =>                        |
   |                                 |        case exp_1 of true => exp_2               |
   |                                 |                   <| false => case vid of match> |
   +---------------------------------+--------------------------------------------------+

• In Appendix A, Figure 17, extend the box for Function-value Bindings by adding

   <if atexp_i>

(with i = 1..m) to each equation in the left box, as the last component of the left-hand sides, and likewise to each match in the right box, as the last component before "=>".

Note that in an fvalbind the guard condition needs to be an atomic expression, in order to avoid syntactic ambiguity.

Static Semantics

Mostly follows from the definition as a derived form. However, guards must be taken into special account wrt checking exhaustiveness and irredundancy:

• In Section 4.11, item 2, add the following sentence:

In the case of the derived form for guarded matches, pat if exp_1 => exp_2, exhaustiveness and irredundancy need to be checked wrt the original form, since the rewriting rule does not maintain those properties. For the purpose of these checks, the guard condition can always be false. Further note that guards may contain side effects and hence change the content of references that have already been matched.

Dynamic Semantics

Follows from the definition as a derived form.

Interactions

Due to potential side effects in guard conditions, this extension renders pattern matching impure. This has a particular consequence on patterns of the form ref atpat, whose behaviour may depend on the evaluation of previous guards. In particular, the following case expression,

   case (i, r) of
       (_, ref true) => 1
     | (2, _) if f() => 2
     | (_, ref false) => 3

is not an exhaustive match, since r may be false, but could get set to true during evaluation of f().

Compatibility

This is a conservative extension.

Implementation

Guards are already available in Alice ML, though with a different choice of keyword. They also exist in Objective Caml.