Значение полиморфизма и "генерация исключения"

Question

Согласно определению стандарта ML (пересмотренный):

Идея состоит в том, что динамическая оценка неэкспансивного выражения не будет генерировать исключение и расширять область памяти, в то время как оценка экспансивного выражения могла бы.

[§4.7, с19; акцент мой]

Я нашел много информации в Интернете о части ref-cell, но почти ничего о части исключения. (Несколько источников указывают, что полиморфное связывание все еще возможно Bind и что это несоответствие может иметь теоретико-типовые последствия и / или последствия реализации, но я не уверен, связано ли это.)

Я смог придумать одну необоснованность, связанную с исключением, которая, если я не ошибаюсь, предотвращается только ограничением значения; но эта необоснованность не зависит от возражения:

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

Итак, может ли кто-нибудь сказать мне, к чему идет определение, и почему оно упоминает исключения?

(Возможно ли, что "создать исключение" означает создание имени исключения, а не создание пакета исключения?)

Answer 1

[Подсказка к ответу pyon за то, что в нем действительно говорится об определении, и за то, что он ввел фразу "порождающие исключения". Я проголосовал за его ответ, но публикую его отдельно, потому что я чувствовал, что его ответ пришел на вопрос с неправильной стороны, в некоторой степени: большая часть этого ответа представляет собой изложение вещей, которые уже предполагаются этим вопросом.]

---

Возможно ли, что "генерировать исключение" означает генерацию имени исключения, а не генерацию пакета исключения?

Да, я так думаю. Хотя в определении обычно не используется слово "исключение", другие источники обычно называют имена исключений просто "исключениями", в том числе в конкретном контексте их генерации. Например, из http://mlton.org/GenerativeException:

В стандарте ML объявления об исключениях называются генеративными, потому что каждый раз, когда объявление исключения оценивается, оно выдает новое исключение.

(И как вы можете видеть там, эта страница постоянно называет имена исключений как "исключения".)

Стандартная библиотека базисов ML также использует "исключение" таким образом. Например, со страницы 29:

С одной стороны, программист может использовать стандартное исключение General.Fail везде, позволяя ему нести строку, описывающую конкретную ошибку. […] Например, одна техника должна иметь функцию sampleFn в структуре Sample поднять исключение Fail "Sample.sampleFn",

Как видите, в этом абзаце дважды используется термин "исключение", один раз для ссылки на имя исключения и один раз для ссылки на значение исключения, полагаясь на контекст, чтобы прояснить значение.

Поэтому для определения вполне разумно использовать фразу "генерировать исключение" для обозначения создания имени исключения (хотя даже в этом случае это, вероятно, небольшая ошибка; определение обычно более точное и формальное, чем это, и обычно указывает, когда он намерен полагаться на контекст для устранения неоднозначности).

Answer 2

Я не теоретик типов и не формальный семантик, но мне кажется, я понимаю, что определение пытается получить с оперативной точки зрения.

Генерируемые исключения ML означают, что всякий раз, когда элемент управления потоком дважды достигает одного и того же объявления исключения, создаются два разных исключения. Мало того, что эти различные объекты находятся в памяти, но эти объекты также экстенсивно неравны: мы можем различать эти объекты путем сопоставления с образцом против конструкторов исключений.

[Между прочим, это показывает важное различие между исключениями ML и исключениями в большинстве других языков. В ML новые классы исключений могут быть созданы во время выполнения.]

С другой стороны, если ваша программа создает один и тот же список целых чисел дважды, у вас может быть два разных объекта в памяти, но ваша программа не может их различить. Они одинаково равны.

---

В качестве примера того, почему генеративные исключения полезны, рассмотрим примерную реализацию MLton универсального типа:

signature UNIV =
sig
  type univ
  val embed : unit -> { inject : 'a -> univ
                      , project : univ -> 'a option
                      }
end

structure Univ :> UNIV =
struct
  type univ = exn

  fun 'a embed () =
    let
      exception E of 'a
    in
      { inject = E
      , project = fn (E x) => SOME x | _ => NONE
      }
    end
end

Этот код вызвал бы огромную дыру в безопасности типа, если бы ML не имел ограничения по значению:

val { inject = inj1, project = proj1 } = Univ.embed ()
val { inject = inj2, project = proj2 } = Univ.embed ()

(*  `inj1` and `proj1` share the same internal exception. This is
 *  why `proj1` can project values injected with `inj1`.
 *  
 *  `inj2` and `proj2` similarly share the same internal exception.
 *  But this exception is different from the one used by `inj1` and
 *  `proj1`.
 *  
 *  Furthermore, the value restriction makes all of these functions
 *  monomorphic.  However, at this point, we don't know yet what these
 *  monomorphic types might be.
 *)

val univ1 = inj1 "hello"
val univ2 = inj2 5

(*  Now we do know:
 *  
 *    inj1 : string -> Univ.univ
 *    proj1 : Univ.univ -> string option
 *    inj2 : int -> Univ.univ
 *    proj2 : Univ.univ -> int option
 *)

val NONE = proj1 univ2
val NONE = proj2 univ1

(*  Which confirms that exceptions are generative.  *)

val SOME str = proj1 univ1
val SOME int = proj2 univ2

(*  Without the value restriction, `str` and `int` would both
 *  have type `'a`, which is obviously unsound.  Thanks to the
 *  value restriction, they have types `string` and `int`,
 *  respectively.
 *)