Search code examples
exceptionlanguage-lawyersmlvalue-restriction

Value polymorphism and "generating an exception"


Per The Definition of Standard ML (Revised):

The idea is that dynamic evaluation of a non-expansive expression will neither generate an exception nor extend the domain of the memory, while the evaluation of an expansive expression might.

[§4.7, p19; emphasis mine]

I've found a lot of information online about the ref-cell part, but almost none about the exception part. (A few sources point out that it's still possible for a polymorphic binding to raise Bind, and that this inconsistency can have type-theoretic and/or implementation consequences, but I'm not sure whether that's related.)

I've been able to come up with one exception-related unsoundness that, if I'm not mistaken, is prevented only by the value restriction; but that unsoundness does not depend on raising an exception:

local
  val (wrapAnyValueInExn, unwrapExnToAnyType) =
    let exception EXN of 'a
    in  (EXN, fn EXN value => value)
    end
in
  val castAnyValueToAnyType = fn value => unwrapExnToAnyType (wrapAnyValueInExn value)
end

So, can anyone tell me what the Definition is getting at, and why it mentions exceptions?

(Is it possible that "generate an exception" means generating an exception name, rather than generating an exception packet?)


Solution

  • [Hat-tip to Eduardo León's answer for stating that the Definition is indeed referring to this, and for bringing in the phrase "generative exceptions". I've upvoted his answer, but am posting this separately, because I felt that his answer came at the question from the wrong direction, somewhat: most of that answer is an exposition of things that are already presupposed by the question.]


    Is it possible that "generate an exception" means generating an exception name, rather than generating an exception packet?

    Yes, I think so. Although the Definition doesn't usually use the word "exception" alone, other sources do commonly refer to exception names as simply "exceptions" — including in the specific context of generating them. For example, from http://mlton.org/GenerativeException:

    In Standard ML, exception declarations are said to be generative, because each time an exception declaration is evaluated, it yields a new exception.

    (And as you can see there, that page consistently refers to exception names as "exceptions".)

    The Standard ML Basis Library, likewise, uses "exception" in this way. For example, from page 29:

    At one extreme, a programmer could employ the standard exception General.Fail everywhere, letting it carry a string describing the particular failure. […] For example, one technique is to have a function sampleFn in a structure Sample raise the exception Fail "Sample.sampleFn".

    As you can see, this paragraph uses the term "exception" twice, once in reference to an exception name, and once in reference to an exception value, relying on context to make the meaning clear.

    So it's quite reasonable for the Definition to use the phrase "generate an exception" to refer to generating an exception name (though even so, it is probably a small mistake; the Definition is usually more precise and formal than this, and usually indicates when it intends to rely on context for disambiguation).