Haskellは一般的に、純粋に関数型言語の例として参照されます。の存在を考えると、これをどのように正当化できSystem.IO.Unsafe.unsafePerformIO
ますか?
編集:「純粋関数型」とは、プログラムの機能部分に不純なコードを導入することは不可能であることを意味していると思いました。
Haskellは一般的に、純粋に関数型言語の例として参照されます。の存在を考えると、これをどのように正当化できSystem.IO.Unsafe.unsafePerformIO
ますか?
編集:「純粋関数型」とは、プログラムの機能部分に不純なコードを導入することは不可能であることを意味していると思いました。
私たちがHaskellと呼ぶ言語
unsafePerformIO
コアHaskell98仕様ではなく、 ForeignFunctionInterface仕様の一部です。純粋に機能的なインターフェースを公開するために、一部のスコープを回避しないローカルな副作用を実行するために使用できます。つまり、タイプチェッカーがそれを実行できないときに効果を非表示にするために使用します(静的保証で効果を非表示にするSTモナドとは異なります)。
「Haskell」と呼ばれる複数の言語を正確に説明するために、以下の画像を検討してください。各リングは、安全性の順に並べられた特定の計算機能のセットに対応し、表現力(つまり、その機能がある場合に記述できるプログラムの数)に相関する領域を備えています。
Haskell 98として知られる言語は、真ん中に指定されており、全体的および部分的な機能を認めています。全体的な機能のみが許可されているAgda(またはEpigram)は、表現力がさらに劣りますが、「より純粋」でより安全です。今日使用しているHaskellには、unsafePerformIOが存在するFFIまでのすべてが含まれています。つまり、現代のHaskellで何でも書くことができますが、外輪からのものを使用すると、内輪によって単純化された安全性とセキュリティの保証を確立するのが難しくなります。
そのため、Haskellプログラムは通常、100%参照透過性のコードから構築されていませんが、デフォルトで純粋な唯一の適度に一般的な言語です。
「純粋に機能的」とは、不純なコードを導入することは不可能であることを意味していると思いました...
本当の答えは、Haskell の一部でunsafePerformIO
はないということです。ガベージ コレクターやランタイム システムは Haskell の一部であるとは言えません。 unsafePerformIO
システムを構築する人々が非常に効果的なハードウェア上で純粋な機能の抽象化を作成できるように、システムに存在します。すべての実際の言語には抜け穴があり、システム ビルダーは C コードやアセンブリ コードに落とし込むよりも効果的な方法で物事を成し遂げることができます。
モナドを介して副作用と I/O が Haskell にどのように適合するかについてのより広い図に関しては、HaskellIO
を考える最も簡単な方法は、Haskell が効果的な計算を記述する純粋な言語であるということだと思います。記述された計算がmain
である場合、ランタイム システムはこれらの効果を忠実に実行します。
unsafePerformIO
安全でない方法で効果を得る方法です。ここで、「安全でない」とは、「安全性はプログラマーによって保証されなければならない」ことを意味し、コンパイラーによって何もチェックされません。あなたが経験豊富なプログラマーであり、厳しい証明義務を喜んで満たす場合は、 を使用できますunsafePerformIO
。しかし、その時点であなたはもう Haskell でプログラミングしているわけではありません。Haskellによく似た安全でない言語でプログラミングしています。
言語/実装は純粋関数型です。いくつかの「エスケープハッチ」が含まれており、使用したくない場合は使用する必要はありません。
unsafePerformIO は、haskell が何らかの形で不純になることを意味するとは思いません。非純粋関数から純粋 (参照透過) 関数を作成できます。
スキップリストを検討してください。うまく機能させるには、不純な関数である RNG へのアクセスが必要ですが、これによってデータ構造が不純になるわけではありません。アイテムを追加してからリストに変換すると、追加したアイテムが与えられるたびに同じリストが返されます。
このため、unsafePerformIO は promisePureIO と考えるべきだと思います。副作用があるため、型システムによって不純とラベル付けされる関数を意味する関数は、型システムによって参照透過として認識されるようになる可能性があります。
ただし、これを保持するには、純粋の定義を少し弱くする必要があることを理解しています。つまり、純粋な関数は参照透過的であり、副作用 (print など) のために呼び出されることはありません。
GHCの最近の拡張であるSafeHaskellは、この質問に対する新しい答えを提供します。unsafePerformIO
はGHCHaskellの一部ですが、安全な方言の一部ではありません。
unsafePerformIO
参照透過性関数を構築するためにのみ使用する必要があります。たとえば、メモ化。このような場合、パッケージの作成者はそれを「信頼できる」とマークします。安全なモジュールは、安全で信頼できるモジュールのみをインポートできます。安全でないモジュールをインポートすることはできません。
詳細情報:GHCマニュアル、SafeHaskell紙
残念ながら、言語は実際の作業を行う必要があり、これは外部環境と話すことを意味します。
良いことは、この「時代遅れの」コードの使用を、プログラムの特定の十分に文書化された部分に制限できることです(そしてそうすべきです)。
私がこれから言おうとしていることを言うと、非常に不人気になるだろうと感じていますが、ここに提示されている (私の意見では間違っている) 情報のいくつかに応答しなければならないと感じました.
unsafePerformIO が FFI の補遺の一部として正式に言語に追加されたのは事実ですが、その理由は論理的ではなく主に歴史的なものです。これは非公式に存在し、Haskell が FFI を持つずっと前から広く使用されていました。これは Haskell の主要な標準の正式な一部ではありませんでした。これは、お気づきのように、あまりにも恥ずかしいことだったからです。どういうわけか、将来のある時点でそれがなくなることを望んでいたと思います。まあ、それは起こっていませんし、私の意見ではそうなるでしょう。
FFI 補遺の開発は、unsafePerformIO が公式言語標準に忍び込むための便利な口実を提供しました。これは、外部 (IE C) コードを呼び出す機能を追加することと比較して、おそらくここではそれほど悪くないように思われるためです (すべての賭けがいずれにせよ、純度と型の安全性を静的に確保することに関してはオフです)。本質的に政治的な理由でここに置くのも非常に便利でした. Haskell が純粋であるという神話を助長したのは、その汚れた「設計の悪い」C、または「設計の悪い」オペレーティング システム、または「設計の悪い」ハードウェア、または..何でも..それは確かに真実です。 unsafePerformIO は、FFI 関連のコードで定期的に使用されますが、その理由は、多くの場合、FFI と実際には Haskell 自体の設計の悪さに関係しています。
したがって、Norman Ramsey が言うように、unsafePerformIO を使用した人が特定の証明義務を満たしていれば、unsafePerformIO を使用しても問題ないという公式の立場になりました (主に、これを行うことで、インライン化や一般的な部分式の削除などの重要なコンパイラ変換が無効にならないということです)。 . これまでのところ、とても良い、またはそう思うかもしれません。本当のキッカケは、おそらく unsafePerformIO の最も一般的な単一のユースケースであるこれらの証明義務を満たすことができないということです。私の推定では、これは実際に存在するすべての unsafePerformIO の 50% をはるかに超えています。私は、「unsafePerformIOハック」として知られる恐ろしいイディオムについて話している.
「unsafePerformIOハック」とは何か、実際のIOライブラリでなぜそれが必要なのかを説明する時間、スペース、または傾向はありませんが、結論として、Haskells IOインフラストラクチャで作業する人々は通常「ロックとハードプレイス"。(Haskell で) 安全な実装を持たない本質的に安全な API を提供するか、安全に実装できる本質的に安全でない API を提供できますが、めったにできないことは、API 設計と両方で安全性を提供することです。実装。「unsafePerformIO ハック」が現実世界のコード (Haskell 標準ライブラリを含む) に現れる気のめいるような規則性から判断すると、ほとんどの人は前者のオプションを 2 つの害の少ないものとして選択し、コンパイラが混乱しないことを願っています。インライン化、cse、またはその他の変換で問題が発生します。
これがすべてそうでなかったらいいのにと思います。残念ながら、そうです。