Consider implementing SML data type definitions:
datatype 'a option = NONE | SOME of 'a
The whole data definition is a pattern in the rest of the module, but the variable a should scope locally over the value constructors which are themselves in scope in the rest of the module.
If we were working with terms, we'd just use a Bind to introduce a scope so that the a ranged over the value constructors.
But since NONE and SOME are constructor names that scope over the rest of the module, what we actually want is to use a LocalBind as a pattern. (This is in some sense a complement to Shift which is all about lifting terms out of scopes whereas this would be limiting the scope of a pattern)
Consider implementing SML data type definitions:
The whole data definition is a pattern in the rest of the module, but the variable
ashould scope locally over the value constructors which are themselves in scope in the rest of the module.If we were working with terms, we'd just use a
Bindto introduce a scope so that thearanged over the value constructors.But since
NONEandSOMEare constructor names that scope over the rest of the module, what we actually want is to use aLocalBindas a pattern. (This is in some sense a complement toShiftwhich is all about lifting terms out of scopes whereas this would be limiting the scope of a pattern)