Haskell では、純粋に機能的なコードから例外をスローできますが、IO コードでしかキャッチできません。
- なんで?
- 他のコンテキストまたは IO モナドのみでキャッチできますか?
- 他の純粋関数型言語はそれをどのように処理しますか?
Haskell では、純粋に機能的なコードから例外をスローできますが、IO コードでしかキャッチできません。
関数内で例外をスローしても、その関数の結果は引数の値と関数の定義以外には依存しないためです。関数は純粋なままです。関数内で例外をキャッチするOTOHは、その関数を純粋な関数ではなくします(または少なくともできます)。
2 種類の例外を見ていきます。1 つ目は非決定論的です。このような例外は、実行時に予期せず発生し、メモリ不足エラーなどを含みます。これらの例外の存在は、例外を生成する関数の意味には含まれません。現実の世界には実際の物理マシンがあり、プログラミングを支援するために使用している抽象化と常に一致するとは限らないため、それらは私たちが対処しなければならない人生の不愉快な事実です.
関数がこのような例外をスローする場合は、関数を評価する特定の試みが値の生成に失敗したことを意味します。関数の結果が (今回呼び出された引数で) 未定義であることを必ずしも意味するわけではありませんが、システムは結果を生成できませんでした。
純粋な呼び出し元内でこのような例外をキャッチできれば、サブ計算が正常に完了したときに 1 つの (底ではない) 値を返し、メモリが不足したときに別の値を返す関数を持つことができます。これは純粋な関数としては意味がありません。関数呼び出しによって計算される値は、その引数の値と関数の定義によって一意に決定される必要があります。サブ計算でメモリが不足しているかどうかに応じて異なるものを返すことができるため、戻り値は他のもの (物理マシンで使用可能なメモリの量、実行中の他のプログラム、オペレーティング システムとそのポリシーなど) に依存します。 .); 定義上、このように動作できる関数は純粋ではなく、Haskell には (通常) 存在できません。
純粋に操作上の失敗のため、関数を評価すると、「本来」生成されるはずの値ではなく、底値が生成される可能性があることを許容する必要があります。それは、Haskell プログラムのセマンティック解釈を完全に台無しにするわけではありません。底がすべての呼び出し元にも底を生成させることがわかっているからです (ただし、計算されるはずの値が必要でない場合を除きますが、その場合は非厳密な評価は、システムがこの関数を評価しようとして失敗しなかったことを意味します)。それは悪いように聞こえますが、計算をIO
モナド内に配置すると、そのような例外を安全にキャッチできます。IO
モナドの値はプログラムの「外部」に依存することが許可されています。実際、それらは世界のあらゆるものに依存して値を変更することができます (これが、IO
値の一般的な解釈の 1 つが、あたかも宇宙全体の表現を渡されたかのようであるという理由です)。IO
そのため、純粋なサブ計算でメモリが不足した場合に値が 1 つの結果を持ち、そうでない場合に別の結果を持つことは完全に問題ありません。
しかし、決定論的例外はどうでしょうか? ここでは、特定の関数を特定の引数セットで評価するときに常にスローされる例外について説明します。このような例外には、ゼロ除算エラーや、純粋な関数から明示的にスローされた例外が含まれます (その結果は、引数とその定義にのみ依存する可能性があるため、一度スローに評価されると、常に同じスローに評価されます)。同じ引数[1])。
このクラスの例外は、純粋なコードでキャッチできるように思われるかもしれません。結局のところ、1 / 0
justの値はゼロ除算エラーです。サブ計算がゼロを渡しているかどうかをチェックすることによってゼロ除算エラーと評価されるかどうかに応じて、関数が異なる結果を持つことができる場合、結果が除算であるかどうかをチェックすることによってこれを行うことができないのはなぜですか-ゼロエラー?
ここで、larsmans がコメントで述べた点に戻ります。純粋関数がどの例外を取得したかを観察できる場合、throw ex1 + throw ex2
その結果は実行順序に依存します。しかし、それはランタイム システム次第であり、同じシステムの 2 つの異なる実行間で変更されることさえあります。おそらく、複数回の実行で最適な戦略に収束しようとするために、実行ごとに異なる並列化戦略を試す高度な自動並列化の実装があります。これにより、例外キャッチ関数の結果は、使用されている戦略、マシン内の CPU の数、マシンの負荷、オペレーティング システムとそのスケジューリング ポリシーなどに依存します。
繰り返しますが、純粋関数の定義は、その引数 (およびその定義) を通じて関数に入る情報のみがその結果に影響を与えるべきであるというものです。非IO
関数の場合、どの例外がスローされるかに影響する情報は、その引数または定義を通じて関数に入らないため、結果に影響を与えることはできません。しかし、IO
モナド内の計算は暗黙的に宇宙全体のあらゆる詳細に依存することが許可されているため、そのような例外をキャッチすることは問題ありません。
2番目の点については、いいえ、他のモナドは例外をキャッチするために機能しません。同じ議論がすべて適用されます。計算は、引数の外部にあるものに依存するMaybe x
か[y]
、依存しないと想定されており、あらゆる種類の例外をキャッチすると、それらの関数の引数に含まれていないものに関するあらゆる種類の詳細が「リーク」します。
モナドについて特に特別なことは何もないことを覚えておいてください。Haskell の他の部分と同じように動作します。モナド型クラスは、ほとんどすべてのモナド実装と同様に、通常の Haskell コードで定義されています。通常の Haskell コードに適用されるすべての同じ規則が、すべてのモナドに適用されます。IO
モナドであるという事実ではなく、それ自体が特別です。
他の純粋な言語が例外のキャッチをどのように処理するかについて言えば、私が使用した経験のある唯一の純粋な言語は Mercury です。[2 ] Mercury は Haskell とは少し異なり、純粋なコードで例外をキャッチできます。
Mercury は論理プログラミング言語であるため、Mercury プログラムは関数に基づいて構築されるのではなく、述語から構築されます。述語への呼び出しは、0、1、またはそれ以上の解を持つことができます (非決定性を得るためにリスト モナドでプログラミングすることに慣れている場合は、言語全体がリスト モナドにあるようなものです)。操作上、Mercury の実行はバックトラッキングを使用して、述語に対するすべての可能なソリューションを再帰的に列挙しますが、非決定論的述語のセマンティクスは、単純に入力引数の各セットに対して単一の結果値を計算する Haskell 関数とは対照的に、入力引数の各セットの解のセット。Haskell と同様に、Mercury は純粋です (I/O を含みますが、わずかに異なるメカニズムを使用します)。したがって、述語への各呼び出しは、引数と述語の定義のみに依存する単一のソリューション セットを一意に決定する必要があります。
Mercury は、各述語の「決定論」を追跡します。常に正確に 1 つのソリューションになる述語が呼び出されますdet
(deterministic の略)。少なくとも1 つの解を生成するものをと呼びmulti
ます。他にもいくつかの決定論クラスがありますが、ここでは関係ありません。
try
ブロックを使用して (またはそれを実装する上位の述語を明示的に呼び出すことによって)例外をキャッチすると、 determinism が発生しcc_multi
ます。ccは「コミットされた選択」の略です。これは、「この計算には少なくとも 1 つの解があり、操作上、プログラムはそのうちの 1 つだけを取得する」ことを意味します。これは、サブ計算を実行し、それが例外を生成したかどうかを確認すると、サブ計算の「通常の」ソリューションとスローされる可能性のあるすべての例外のセットの和集合であるソリューション セットがあるためです。「考えられるすべての例外」には実行時に発生する可能性のあるすべてのエラーが含まれ、そのほとんどが実際には発生しないため、このソリューション セットを完全に実現することはできません。そこには'try
代わりに、解決策を提供するだけです(通常の解決策、またはすべての可能性が調査され、解決策も例外もなかったという兆候、またはたまたま発生した最初の例外)。
コンパイラは決定論を追跡するためtry
、完全なソリューション セットが重要なコンテキストで呼び出すことはできません。たとえば、例外が発生しないすべてのソリューションを生成するために使用することはできません。たとえば、コンパイラは、cc_multi
1 つだけを生成する呼び出しに対してすべてのソリューションが必要であると不平を言うからです。ただし、述語から呼び出すこともできませんdet
。コンパイラーは、det
述語 (厳密に 1 つのソリューションを持つことになっている) がcc_multi
複数のソリューションを持つ呼び出しを行っていると不平を言うからです (何がわかるかだけです)。それらの1つです)。
では、一体これがどのように役立つのでしょうか。まあ、あなたはmain
(そしてそれが有用であればそれが呼び出す他のもの)を として宣言cc_multi
することができ、問題なく呼び出すことができますtry
。これは、理論上はプログラム全体に複数の「解」があることを意味しますが、実行すると解が生成されます。これにより、ある時点でメモリが不足した場合に異なる動作をするプログラムを作成できます。しかし、より多くのメモリを使用して計算されたであろう「実際の」結果はまだ解決策セットにあるため、宣言的セマンティクスを損なうことはありません (プログラムが実際に実行するときにメモリ不足の例外がまだ解決策セットにあるのと同じように)。値を計算する)、1 つの任意の解しか得られないだけです。
(解決策は 1 つだけあります) は、 (複数の解決策がありますが、そのうちの 1 つしか持てませんdet
) とは異なる方法で処理されることが重要です。cc_multi
Haskell で例外をキャッチすることについての推論と同様に、「コミットされた選択」のコンテキストで例外をキャッチすることは許可されません。または、現実世界からの情報に応じて異なるソリューション セットを生成する純粋な述語を取得することができます。アクセスできません。のcc_multi
決定論により、プログラムが無限のソリューション セットを生成するかtry
のようにプログラムを作成することができ(ほとんどの場合、ありそうもない例外のマイナー バリアントでいっぱいです)、セットから複数のソリューションを実際に必要とするプログラムを作成することができなくなります。[3]
[1] それを評価する場合を除き、最初に非決定論的エラーが発生します。実生活は苦痛です。
[2] 純粋性を強制せずに単にプログラマーに純粋性を使用することを奨励する言語 (Scala など) は、好きな場所で I/O を実行できるようにするのと同じように、好きな場所で例外をキャッチできるようにする傾向があります。
[3] 「コミットされた選択」の概念は、Mercury が純粋な I/O を処理する方法ではないことに注意してください。そのために、マーキュリーは、「コミットされた選択」決定論クラスと直交する一意の型を使用します。
delnan がコメントで言及している論文と、この前の質問への回答は、例外のみをキャッチする十分な理由を確かに提供しIO
ます。
ただし、評価の順序を守る、単調性を破るなどの理由が、直感的なレベルでは説得力がない理由もわかります。いずれかが大部分のコードに大きな害を及ぼす可能性があることを想像するのは困難です。そのため、例外処理は明確に非ローカルな種類の制御フロー構造であり、純粋なコードで例外をキャッチできると、その目的でそれらを (誤) 使用することが可能になることを思い出してください。
これがどのような恐怖を伴うのかを正確に説明させてください.
まず、使用する例外タイプを定義し、catch
純粋なコードで使用できるバージョンを定義します。
newtype Exit a = Exit { getExit :: a } deriving (Typeable)
instance Show (Exit a) where show _ = "EXIT"
instance (Typeable a) => Exception (Exit a)
unsafeCatch :: (Exception e) => a -> (e -> a) -> a
unsafeCatch x f = unsafePerformIO $ catch (seq x $ return x) (return . f)
Typeable
これにより、介在する式の同意なしに、任意の値をスローして、外側のスコープからキャッチできます。たとえば、Exit
高階関数に渡すものの中に throw を隠して、その評価によって生成された中間値でエスケープすることができます。賢明な読者は、これがどこに向かっているのか、今では理解しているかもしれません。
callCC :: (Typeable a) => ((a -> b) -> a) -> a
callCC f = unsafeCatch (f (throw . Exit)) (\(Exit e) -> e)
はい、それは実際に機能しますが、式全体が評価されるたびに継続を使用する必要があるという警告があります。これを試すかdeepseq
、軌道からの核攻撃があなたの速度よりも速い場合に使用する場合は、そのことを覚えておいてください.
見よ:
-- This will clearly never terminate, no matter what k is
foo k = fix (\f x -> if x > 100 then f (k x) else f (x + 1)) 0
しかし:
∀x. x ⊢ callCC foo
101
内部からのエスケープmap
:
seqs :: [a] -> [a]
seqs xs = foldr (\h t -> h `seq` t `seq` (h:t)) [] xs
bar n k = map (\x -> if x > 10 then k [x] else x) [0..n]
評価を強制する必要があることに注意してください。
∀x. x ⊢ callCC (seqs . bar 9)
[0,1,2,3,4,5,6,7,8,9]
∀x. x ⊢ callCC (seqs . bar 11)
[11]
…うーん。
さて、これについては二度と話さないようにしましょう。