13

現在、非常に恐ろしい関数unsafeCoerceを使用している状況があります。幸いなことに重要なことではありませんが、これがこの関数の安全な使用法であると思われるのか、それとも他の人が知っているこの特定の問題を解決する別の方法があるのでしょうか。

私が持っているコードは次のようなものです：

data Token b = Token !Integer

identical :: Token a -> Token b -> Bool
identical (Token a) (Token b) = a == b

data F a = forall b. F (Token b) (a -> b)

retrieve :: Token b -> F a -> Maybe (a -> b)
retrieve t (F t' f) = if identical t t' then Just (unsafeCoerce f) else Nothing

注意すべき2つの追加事項は、これらのトークンは、整数の供給が一意であることを確認するために使用するモナド内で使用されることです（つまり、同じトークンを2回作成しない）。また、STモナドと同じように、forallの定量化されたシャドウ型変数を使用して、（モジュールで公開するメソッドのみが使用されていると仮定して）トークンを返す方法がないことを確認します（実際には、 F）型エラーではなくモナドから。また、トークンコンストラクターも公開していません。

私が見る限り、これはunsafeCoerceの安全な使用法であると思います。私が強制している値は、実際には私が強制しているタイプとまったく同じであるというかなり高い確信を持って言えるでしょう。 、しかし私は間違っているかもしれません。また、Data.Typeableを使用してみましたが、これはうまく機能しますが、現時点では、Typeableの制約を回避するためにこれを試みています。特に、gcastは多くの点で同様のことを行うようであり、区別するためにトークンが必要です。同じタイプの異なるF。

ヘルプ/アドバイスをありがとうございました。

4

2 に答える 2

14

Data.Dynamicのスタイルに広く従って、制限された形式の動的型付けを実装しました。つまり、（不透明な）値をその型の証拠とペアリングします。実行時に、データとともに出荷した証拠に基づいて、安全でない強制を行うことができます。

fromDyn (Dynamic t v) def
  | typeOf def == t = unsafeCoerce v
  | otherwise       = def

これは、長い歴史を持つ標準的なアプローチであり、以下に戻ります。

マルティン・アバディ、ルカ・カーデリ、ベンジャミン・ピアス、ゴードン・プロトキン。静的に型付けされた言語での動的型付け。プログラミング言語とシステムに関するACMトランザクション、13（2）：237–268、1991年4月。

このアプローチの安全性は、ランタイムタイプのトークンが偽造できないことに依存しています。あなたの場合、誰でも2つのタイプに相当するトークンを作成できます。タイプからトークンへの1対1のマッピングを保証し、悪意のあるユーザーが誤ったトークンを作成できないようにする必要があります。GHCの場合、Typeableインスタンス（およびモジュールの抽象化）を信頼します。

于 2013-01-14T16:46:01.480 に答える
9

それ自体は安全ではありません。

oops :: F Bool
oops = F (Token 12) not

bad :: Token Int
bad = Token 12

*Token> maybe 3 ($ True) $ retrieve bad oops
1077477808

F abは存在記号型であり、どの型が入ったのかわかりません。identicalの型パラメータを気にしないので、の最初の引数から提供されたものが、に入力されたものと関係があるTokenかどうかを確認できません。bretrieveF a

あなたの保護かどうか

注意すべき2つの追加事項は、これらのトークンは、整数の供給が一意であることを確認するために使用するモナド内で使用されることです（つまり、同じトークンを2回作成しない）。また、STモナドと同じように、forallの定量化されたシャドウ型変数を使用して、（モジュールで公開するメソッドのみが使用されていると仮定して）トークンを返す方法がないことを確認します（実際には、 F）型エラーではなくモナドから。また、トークンコンストラクターも公開していません。

実際に安全にするのに十分な強さですが、それを見ないとわかりません。実際Tokenに計算の外部でsを作成できず、のInteger値がToken型パラメーターを一意に特徴付ける場合は、安全です。

于 2013-01-14T16:44:42.257 に答える