26

コンパイルするために-XUndecidableInstancesを必要とするHaskellコードをいくつか書きました。私はそれがなぜ起こるのか、違反されている特定の条件があり、したがってGHCが叫ぶことを理解しています。

しかし、タイプチェッカーが実際にハングしたり、無限ループに陥ったりするような状況に遭遇したことはありません。

非終了インスタンス定義はどのように見えますか？例を挙げていただけますか？

4

2 に答える 2

40

HQからのこの論文には、古典的でやや憂慮すべき例（関数従属性との相互作用を含む）があります。

class Mul a b c | a b -> c where
  mul :: a -> b -> c
instance Mul a b c => Mul a [b] [c] where
  mul a = map (mul a)

f b x y = if b then mul x [y] else y

mul x [y]と同じタイプが必要なyので、とっx :: xてy :: y、

instance Mul x [y] y

与えられた例によれば、これは私たちが持つことができます。もちろん、私たちはそのようなものをy ~ [z]取る必要がありますz

instance Mul x y z

すなわち

instance Mul x [z] z

そして、私たちはループしています。

Petrの回答の明らかに病理学的なインスタンスとは異なり、そのインスタンスはその再帰が構造的に減少Mulしているように見えるため、気がかりです。それでも、GHCループを作成します（ハングを回避するために退屈なしきい値が開始されます）。

問題は、いつかどこかで言及したと思いますが、機能的にに依存y ~ [z]しているという事実にもかかわらず、識別が行われることです。関数従属性に関数記法を使用した場合、制約がオカレンスチェックに違反しているとして置換を指示して拒否することがわかります。zyy ~ Mul x [y]

興味をそそられて、私はこれに旋風を与えると思いました、

class Mul' a b where
  type MulT a b
  mul' :: a -> b -> MulT a b

instance Mul' a b => Mul' a [b] where
  type MulT a [b] = [MulT a b]
  mul' a = map (mul' a)

g b x y = if b then mul' x [y] else y

有効にUndecidableInstancesすると、ループがタイムアウトするまでにかなりの時間がかかります。無効にUndecidableInstancesしても、インスタンスは引き続き受け入れられ、タイプチェッカーはループしますが、カットオフははるかに迅速に行われます。

だから...面白い古い世界。

于 2013-02-02T13:00:27.927 に答える
20

例えば：

{-# LANGUAGE UndecidableInstances #-}

class C a where
    f :: a -> a

instance C [[a]] => C [a] where
    f = id

g x = x + f [x]

何が起こっているのか：f [x]コンパイラーを入力するときはx :: C [a]、いくつかのことを確認する必要がありaます。インスタンス宣言は、それがタイプでもある場合にのみx、タイプである可能性があることを示しています。したがって、コンパイラは、などが無限ループに陥ることを確認する必要があります。C [a]C [[a]]x :: C [[a]]

UndecidableInstancesプラグマをローカルで使用すると、コンパイルの終了にグローバルな影響を与える可能性もありますか？も参照してください。

于 2013-02-02T11:12:18.653 に答える