5

標準 ML の定義 (改訂)ごとに:

非拡張式の動的評価は例外を生成せず、メモリのドメインを拡張することもありませんが、拡張式の評価は例外を生成する可能性があります。

[§4.7、p19; 強調鉱山]

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

では、定義が何を目指しているのか、なぜ例外について言及しているのか、誰か教えてもらえますか?

(「例外を生成する」とは、例外パケットを生成するのではなく、例外名を生成することを意味する可能性はありますか?)

4

2 に答える 2

2

私は型理論家でも正式な意味論者でもありませんが、運用上の観点から定義が何を達成しようとしているのかを理解していると思います。

ML 例外が生成的であるということは、フローの制御が同じ例外宣言に 2 回到達するたびに、2 つの異なる例外が作成されることを意味します。これらのオブジェクトはメモリ内にあるだけでなく、拡張的にも等しくありません。これらのオブジェクトは、例外コンストラクターに対するパターン マッチングによって区別できます。

[ちなみに、これは ML 例外と他のほとんどの言語の例外との重要な違いを示しています。ML では、実行時に新しい例外クラスを作成できます。]

一方、プログラムが同じ整数のリストを 2 回作成する場合、メモリ内に 2 つの異なるオブジェクトが存在する可能性がありますが、プログラムにはそれらを区別する方法がありません。それらは拡張的に等しいです。

生成例外が役立つ理由の例として、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.
 *)
于 2015-07-12T18:06:08.100 に答える
2

[定義が実際にこれを参照していると述べ、「生成的例外」というフレーズを導入したEduardo Leónの回答に感謝します。私は彼の答えに賛成しましたが、彼の答えが質問に対して間違った方向から来たと感じたので、これを個別に投稿しています。その答えのほとんどは、質問によってすでに前提とされていることの説明です.]

「例外を生成する」とは、例外パケットを生成するのではなく、例外名を生成することを意味する可能性はありますか?

はい、そう思います。定義では通常、「例外」という言葉を単独で使用することはありませんが、他の情報源では、例外を生成する特定のコンテキストを含め、例外名を単に「例外」と呼ぶのが一般的です。たとえば、http://mlton.org/GenerativeExceptionから:

標準 ML では、例外宣言が評価されるたびに新しい例外が生成されるため、例外宣言は生成的であると言われています。

(そして、そこにあるように、そのページでは一貫して例外名を「例外」と呼んでいます。)

Standard ML Basis Libraryも同様に、このように「例外」を使用します。たとえば、29ページから：

極端な例として、プログラマは標準例外をGeneral.Failあらゆる場所で使用して、特定の障害を説明する文字列を保持させることができます。[…] たとえば、1 つの手法はsampleFn、構造内の関数にSample例外を発生させることですFail "Sample.sampleFn"。

ご覧のとおり、この段落では「例外」という用語を 2 回使用しています。1 回は例外名を参照する場合で、もう 1 回は例外値を参照する場合です。意味を明確にするためにコンテキストに依存しています。

したがって、定義で「例外を生成する」というフレーズを使用して例外名を生成することを指すのは非常に合理的です(ただし、そうであっても、おそらく小さな間違いです。定義は通常、これよりも正確で形式的であり、通常、いつ発生するかを示します)。あいまいさを解消するためにコンテキストに依存することを意図しています)。

于 2015-07-12T19:13:46.593 に答える