1

IO 操作に裏打ちされたジェネリック プロパティ マップを書きたいとしますが、何らかの理由で値型をポリモーフィックにする必要があります。

type Key = Int
get:: Key -> v -> IO v -- Takes a key and a default value, return the associated value
put:: Key -> v -> IO () -- store (Key,v) pair doing some IO

自由定理はそれを必要とgetしput、この場合も些細なことだけを行いますか? もしそうなら、ghc の型システムをごまかして、実際の型インデックス付き IO データベースを実装できますか?

4

1 に答える 1

8

一般に ではおかしなことが起こるIOので、 を含む自由定理の厳密な概念はないと思いますIO。とにかく、それが実装されていることについて私が知っていることからIO、関数が機能すると仮定して

  1. クラッシュする可能性のあるものは何もありません (無意味なポインター演算を行って v 型の値を生成するなど)。
  2. 安全でない関数を使用しない (一般に自由定理のような推論を破る)、
  3. ボトムを返さない (例:undefinedまたは例外) および
  4. 最終的に「戻る」</li>

その場合、「返された」値がパラメーターになります。

ただし、これは、を使用して型索引付きデータベースを実装することができないIOことを意味します。

Typeable a制約があれば可能です。その場合、予想される自由定理は成り立たず、get関数はデフォルト値以外のものを返すことができます。

于 2013-02-28T15:57:15.567 に答える