Generalizing layered patterns to conjunctive patterns

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 generalising layered to patterns to conjunctive patterns.

Motivation and Example

SML provides layered patterns vid as pat to allow naming a value and simultaneously matching its structure. The name must be put first. However, depending on the situation, it often is more convenient to put the name last.

Instead of adding a second syntactic form, we propose generalizing layered patterns to arbitrary conjunctive patterns pat_1 as pat_2, which trivially supports both forms, while also eliminating grammar problems that exist with the current syntax (it is not LR(1)).

Assumptions

None.

Syntax

Defined by the following modification to the Definition:

• In Section 2.8, Figure 3, and in Appendix B, Figure 22, replace the production for layered patterns with:

   pat_1 as pat_2    conjunctive

• In Appendix A, Figure 16, remove the box for pattern rows.

Static Semantics

Defined by the following modification to the Definition:

• In Section 4.10, Patterns, replace rule 43 with:

   C |- pat_1 => (VE_1,tau)    C |- pat_2 => (VE_2,tau)    Dom VE_1 \cap Dom VE_2 = 0
   ----------------------------------------------------------------------------------   (43)
                       C |- pat_1 as pat_2 => (VE_1 + VE_2,tau)

• In Section 4.11, add the following bullet:

Every pattern of the form pat_1 as pat_2 must be consistent, i.e. there must exist at least one value that is matched by both patterns.

Dynamic Semantics

Defined by the following modifications to the Definition:

• In Section 6.7, Patterns, replace rule 149 with:

   E,v |- pat_1 => VE_1    E,v |- pat_2 => VE_2/FAIL
   -------------------------------------------------   (149)
      E,v |- pat_1 as pat_2 => (VE_1 + VE_2)/FAIL

• Add the following rule:

       E,v |- pat_1 => FAIL
   -----------------------------   (149a)
   E,v |- pat_1 as pat_2 => FAIL

Interactions

None.

Compatibility

This is a conservative extension.

Implementation

Pattern matching is not complicated significantly by the change. It actually simplifies parsing. The extension has already been implemented in Alice ML.