5

型推論中に強制 (別名暗黙の変換) を推論する方法を知りたいです。私は、Bastiaan Heeren によるTop Quality Type Error Messagesで説明されている型推論スキームを使用していますが、一般的な考え方はおそらくすべての Hindley-Milner 風のアプローチで同じであると思います。

強制はオーバーロードの一種として扱うことができるように思えますが、このホワイト ペーパーで説明するオーバーロードのアプローチでは、コンテキストが戻り値の型に課す要件に基づくオーバーロードを (少なくとも私が理解できる方法では) 考慮していません。強要には必須。また、このようなアプローチでは、同一性強制を優先することや、強制可能性の推移的閉鎖を尊重することが難しくなる可能性があることも懸念しています。各強制可能な式、たとえばeをcoerce ( e ) にシュガーリングしていますが、それを coerce(coerce(coerce(... coerce( e )) にシュガーリングしています。) ...))) 強制の最大ネスティングに等しい深さについては、ばかげているように見えます。また、強制可能性の関係を、深さがコンテキストから独立している有限の推移的なクロージャーを持つ何かに制限します。

4

3 に答える 3

3

これに対する良い答えが得られることを願っています。

リンク先の論文はまだ読んでいませんが、面白そうです。アドホック ポリモーフィズム (基本的にオーバーロード) が Haskell でどのように機能するかを調べましたか? Haskell の型システムは、HM にその他の機能を追加したものです。それらの利点の 1 つは、型クラスです。型クラスは、オーバーロードを提供します。Haskeller が呼ぶように、アドホック ポリモーフィズムです。

最も広く使用されている Haskell コンパイラである GHC では、型クラスは実行時に辞書を渡すことによって実装されます。ディクショナリにより、ランタイム システムは型から実装へのルックアップを実行できます。おそらく、jhcは超最適化を使用してコンパイル時に適切な実装を選択できると思われますが、Haskell が許可できる完全なポリモーフィックなケースを処理できるかどうかは懐疑的であり、正確性を主張する正式な証明や論文も知りません。

あなたの型推論は、他のランク n ポリモーフィック アプローチと同じ問題に遭遇するようです。追加の背景として、ここでいくつかの論文を読みたいと思うかもしれません: "型に関する論文" までスクロールし ます。

ランク n ポリモーフィズムと型チェックの問題に関するこの論文は、興味深い考えを引き起こすはずです: http://research.microsoft.com/~simonpj/papers/higher-rank/

より良い答えを提供できればいいのに！幸運を。

于 2008-09-16T06:24:33.637 に答える
1

私の経験では、すべての用語を直感的に甘やかすことは魅力的ではないように思えますが、追求する価値はあります。

永続ストレージへの関心から、式と原子値の混合の問題を検討する遠回りの道をたどりました。これをサポートするために、型システムでそれらを完全に分離することにしました。したがって、Int、Char などは、整数値と文字値のみの型コンストラクターです。式の型は、多相型コンストラクタ Exp で形成されます。たとえば、Exp Int は、1 ステップで Int に減少する値を指します。

これとあなたの質問との関連性は、評価を検討するときに生じます。基になるレベルでは、原子値を必要とするプリミティブがあります: COND、addInt など。これを式の強制と呼ぶ人もいますが、私は単純に異なる型の値の間のキャストと見なすことを好みます。

課題は、明示的な削減指令を必要とせずにこれを実行できるかどうかを確認することです。1つの解決策は、あなたが示唆するとおりです。つまり、強制をオーバーロードの形式として扱うことです。

入力スクリプトがあるとします。foo x

次に、砂糖漬けの後、これは次のようになります。(coerce foo) (coerce x)

ここで、非公式に：

coerce :: a -> b
coerce x = REDUCE (cast x) if a and b are incompatible
x                          otherwise

したがって、強制は同一性またはキャストの適用のいずれかです。ここで、bは特定のコンテキストの戻り値の型です。

キャストを型クラス メソッドとして扱うことができるようになりました。

class Cast a, b where {cast :: a -> b };
-- ¬:: is an operator, literally meaning: don’t cast
--(!) is the reduction operator. Perform one stage of reduction.

-- Reduce on demand
instance Cast Exp c, c where { inline cast = ¬::(!)(\x::(Exp c) -> ¬::(!)x) };

¬::注釈は、強制的な構文シュガーリングを抑制するために使用されます。

意図はCast、変換の範囲を拡張するために の他のインスタンスを導入できることですが、これについては調べていません。おっしゃるとおり、重複するインスタンスが必要なようです。

于 2010-01-12T10:16:11.487 に答える
0

何を求めているのか、もう少し詳しく教えていただけますか？

私にはちょっとした考えがあります。私の考えが正しければ、この答えで十分です。あなたは言語を作成している誰かの観点からこれについて話していると思います。その場合、例としてActionScript3のような言語を見ることができます。AS3では、2つの異なる方法で型キャストできます。1）NewType（object）、または2）ObjectasNewType。

実装の観点から、私がイメージングするすべてのクラスは、変換できるタイプに変換する独自の方法を定義する必要があります（配列は実際には整数に変換できません...またはできますか？）。たとえば、Integer（myArrayObject）を試し、myArrayObjectが整数への変換方法を定義していない場合は、例外をスローするか、そのままにして、キャストされていない元のオブジェクトを渡すことができます。

私の答え全体は完全にずれている可能性があります:-Dこれがあなたが探しているものではない場合は私に知らせてください

于 2008-09-16T06:19:49.390 に答える