以前、を使用してコードを書いたときにUndecidableInstances、非常に奇妙なことに遭遇しました。意図せず、タイプチェックを行うべきではないと思っていたのに、タイプチェックを行うコードを作成してしまったのです。
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
data Foo = Foo
class ConvertFoo a b where
convertFoo :: a -> b
instance (ConvertFoo a Foo, ConvertFoo Foo b) => ConvertFoo a b where
convertFoo = convertFoo . (convertFoo :: a -> Foo)
evil :: Int -> String
evil = convertFoo
具体的には、convertFoo関数は与えられた場合に型チェックを行う。どれでも生産するための入力どれでも出力は、関数 によって示されますevil。最初は、おそらく を誤って実装してしまったのだろうと思いましたunsafeCoerceが、それは正しくありません。実際にconvertFoo関数を呼び出そうとすると (たとえば、 のような操作を行うことによってevil 3)、単に無限ループに陥ります。
私ちょっと何が起こっているのか漠然と理解しています。この問題についての私の理解は次のようになります。
ConvertFoo私が定義したインスタンスは、どれでも入力と出力、aおよびは、およびbからの変換関数が存在しなければならないという 2 つの追加制約によってのみ制限されます。a -> FooFoo -> b- どういうわけか、その定義は任意の入力および出力タイプに一致できるので、 の呼び出しは、とにかくそれが唯一利用可能な定義であるため、それ自体
convertFoo :: a -> Fooの定義そのものを選択しているように見えます。convertFoo - 関数は自分自身を無限に呼び出すため
convertFoo、決して終了しない無限ループに入ります。 - は
convertFoo決して終了しないので、その定義の型はbottomなので、技術的にいずれの型も違反されず、プログラムは型チェックされます。
さて、上記の理解が正しいとしても、プログラム全体がなぜ型チェックされるのかまだわかりません。具体的には、そのようなインスタンスが存在しないため、ConvertFoo a FooおよびConvertFoo Foo b制約が失敗すると予想されます。
私するインスタンスを選択するときに制約は重要ではないことを (少なくともあいまいに) 理解しています。インスタンスはインスタンス ヘッドのみに基づいて選択され、その後制約がチェックされます。そのため、可能な限りConvertFoo a b許容度の高いインスタンスであるため、これらの制約が問題なく解決される可能性があることがわかりました。ただし、そうすると、同じ制約セットを解決する必要があり、その結果、型チェッカーが無限ループに陥り、GHC がコンパイル時にハングするか、スタック オーバーフロー エラー (後者は以前に見たことがあります) が発生すると思います。
しかし、明らかに、型チェッカーはないループは、うまく底まで到達し、コードが正常にコンパイルされるからです。なぜでしょうか? この特定の例では、インスタンス コンテキストはどのように満たされるのでしょうか? これによって型エラーが発生したり、型チェック ループが生成されたりしないのはなぜでしょうか?
ベストアンサー1
これは素晴らしい質問だと私は心から同意します。これは、型クラスに関する私たちの直感が現実とどのように異なるかを物語っています。
型クラスの驚き
ここで何が起こっているのかを確認するために、次の型シグネチャの賭け金を上げますevil:
data X
class Convert a b where
convert :: a -> b
instance (Convert a X, Convert X b) => Convert a b where
convert = convert . (convert :: a -> X)
evil :: a -> b
evil = convert
Covert a bこのクラスのインスタンスは 1 つしかないため、明らかにインスタンスが選択されています。型チェッカーは次のように考えています。
Convert a X...の場合、真となります。Convert a X真実である[仮定により真実である]- そして
Convert X X真実であるConvert X X...の場合、真となります。Convert X X真実である[仮定により真実である]Convert X X真実である[仮定により真実である]
Convert X b...の場合、真となります。Convert X X真実である[上記から真実である]- そして
Convert X b真実である[仮定により真実である]
タイプチェッカーは私たちを驚かせました。私たちConvert X Xはそのようなものを定義していないので、真であるとは予想していませんでした。しかし、(Convert X X, Convert X X) => Convert X Xこれは一種のトートロジーです。つまり、自動的に真となり、クラスでどのようなメソッドが定義されていても真となります。
これは、型クラスのメンタルモデルと一致しないかもしれません。この時点でコンパイラが驚いて、Convert X Xインスタンスが定義されていないため が真にならないと文句を言うことが予想されます。コンパイラが に立ち止まりConvert X X、 が真になる別の場所を探しConvert X X、 が真になる他の場所がないため諦めることが予想されます。しかし、コンパイラは再帰が可能です。再帰、ループ、チューリング完全です。
私たちは、型チェッカーにこの機能を与え、 でそれを実現しましたUndecidableInstances。ドキュメントにコンパイラをループに送る可能性があると記載されている場合、最悪の事態を想定するのは簡単で、悪いループは常に無限ループであると想定しました。しかし、ここではさらに致命的なループ、つまり終了するただし、驚くべき方法を除いて。
（これはダニエルのコメントでさらに顕著に示されています：
class Loop a where
loop :: a
instance Loop a => Loop a where
loop = loop
。
決定不能性の危険性
これはまさに許可される状況ですUndecidableInstances。その拡張機能をオフにして、FlexibleContexts（本質的には文法上の無害な拡張機能）をオンにすると、パターソンの条件:
...
Constraint is no smaller than the instance head
in the constraint: Convert a X
(Use UndecidableInstances to permit this)
In the instance declaration for ‘Convert a b’
...
Constraint is no smaller than the instance head
in the constraint: Convert X b
(Use UndecidableInstances to permit this)
In the instance declaration for ‘Convert a b’
「インスタンス ヘッドより小さくない」ですが、これを「このインスタンスは、それ自体の主張を証明するために使用され、多くの苦悩と歯ぎしりと入力を引き起こす可能性があります」と書き直すこともできます。Paterson 条件は、インスタンス解決でのループを防止します。ここでの違反は、これらがなぜ必要なのかを示しており、これらがなぜ十分であるかについては、おそらく何らかの論文を参照することができます。
底を打つ
プログラムが実行時に無限ループする理由については、evil :: a -> bHaskell の型チェッカーを信頼しており、ボトム以外に存在できる値がないため、無限ループするか、例外をスローするか、一般的にボトムアウトするしかないという退屈な答えがありますa -> b。
もっと興味深い答えは、がConvert X Xトートロジー的に正しいので、そのインスタンス定義はこの無限ループであるということです。
convertXX :: X -> X
convertXX = convertXX . convertXX
同様にインスタンス定義を拡張することもできますConvert A B。
convertAB :: A -> B
convertAB =
convertXB . convertAX
where
convertAX = convertXX . convertAX
convertXX = convertXX . convertXX
convertXB = convertXB . convertXX
この驚くべき動作、およびこれらの動作を回避するためにインスタンス解決が（拡張なしでデフォルトで）どのように制約されているかは、おそらく Haskell の型クラス システムがまだ広く採用されていない理由として十分考えられるでしょう。その印象的な人気とパワーにもかかわらず、型クラスには奇妙な部分があり（ドキュメント、エラー メッセージ、構文、または基礎となるロジックにさえ）、特に私たち人間の型レベルの抽象化に関する考え方に合わないようです。