Disallow non-exhaustive patterns in polymorphic bindings
From Successor ML
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.
