Haskell/GHC UndecidableInstances - 非終止類型檢查的例子？

Question

我寫了一些需要-XUndecidableInstances編譯的Haskell代碼。我明白爲什麼會發生這種情況，有一個違反的條件，因此GHC大叫。

但是，我從來沒有遇到類型檢查程序實際上會掛起或無限循環結束的情況。

什麼是非終止實例定義的樣子 - 你能舉個例子嗎？

Answer 1

例如：

{-# 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]]等，並陷入無限循環。

又見Can using UndecidableInstances pragma locally have global consequences on compilation termination?

Answer 2

有一個經典的，有點令人震驚的例子（涉及函數依賴的相互作用）在this paper from HQ：我們需要mul x [y]具有相同類型y

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 

，所以，服用x :: x和y :: y，我們需要

instance Mul x [y] y 

whi按照給定的例子，我們可以擁有。當然，我們必須採取y ~ [z]一些z這樣

instance Mul x y z 

即

instance Mul x [z] z 

，我們正處在一個循環。

這是令人不安的，因爲Mul實例看起來像它的遞歸結構減少，不像Petr的答案中的明確病理實例。然而，它使得GHC循環（無聊閾值踢入避免懸掛）。

麻煩，因爲我敢肯定，我曾經在某個地方提到過，即使在z在功能上取決於y，但確定y ~ [z]。如果我們爲功能依賴項使用功能符號，我們可能會看到約束條件爲y ~ 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被禁用，實例仍然被接受，類型檢測器仍然循環，但截斷髮生得更快。

所以......有趣的舊世界。