Disallow non-exhaustive patterns in polymorphic bindings

From Successor ML

Jump to: navigation, search

Contents

Introduction

We propose to disallow polymorphic bindings to have non-exhaustive patterns.

Motivation

In order maintain to soundness of polymorphic typing in the presence of effects, polymorphism is restricted to non-expansive bindings. Non-expansiveness is a syntactic condition on expressions that is sufficient to guarantee absence of effects (including exceptions) during their evaluation.

However, an exception may still occur if the pattern in the binding is not exhaustive. That behaviour is somewhat inconsistent, and more importantly, unnecessarily complicates typed compilation schemes, like used by several SML compilers. Some of these compilers rule out non-exhaustive patterns in polymorphic bindings. We propose to bless their behaviour. That is, pathological programs like

   val x::xs = []

but also

   val x::xs = [NONE, NONE]

will no longer be valid. Note that such declarations are rather useless, and can easily be rewritten.

Assumptions

None.

Syntax

Unaffected.

Static Semantics

Defined by the following modifications to the Definition:

  • In Section 4.8, change the rules for obtaining alpha^(k) to:
   alpha^(k) = tyvars tau \ tyvars C,  if pat exhaustive and exp non-expansive in C;
               (),                     otherwise.
Further, add the following sentence:
   A pattern is /exhaustive/ if it matches all values (of the right type, cf. Section 4.11).

Dynamic Semantics

Unaffected.

Interactions

None.

Compatibility

Not conservative, but very unlikely to break any practical program. Already implemented in SML/NJ and TILT.

Implementation

Not difficult, but requires pattern checks to be performed interleaved with type checking.

Personal tools