हास्केल/जीएचसी अनिश्चित इंस्टेंस - गैर-समाप्ति प्रकार की जांच के लिए उदाहरण?

Question

मैंने कुछ हास्केल कोड लिखे हैं जिन्हें संकलित करने के लिए -XUndecidableInstances की आवश्यकता है। मुझे समझ में आता है कि ऐसा क्यों होता है, कि एक निश्चित शर्त है जिसका उल्लंघन किया जाता है और इसलिए जीएचसी चिल्लाता है।

हालांकि, मैं कभी ऐसी परिस्थिति में नहीं आया हूं जहां टाइप चेकर वास्तव में लटका होगा या अंतहीन पाश में घुमाएगा।

गैर-समाप्ति उदाहरण परिभाषा कैसा दिखता है - क्या आप एक उदाहरण दे सकते हैं?

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] टाइपिंग संकलक कुछ a के लिए कि x :: C [a] सुनिश्चित करने के लिए की जरूरत है। उदाहरण घोषणा में कहा गया है कि xC [a] प्रकार का हो सकता है यदि यह C [[a]] प्रकार भी है। तो संकलक को यह सुनिश्चित करने की आवश्यकता है कि x :: C [[a]], आदि और एक अनंत लूप में पकड़ा जाता है।

भी देखें Can using UndecidableInstances pragma locally have global consequences on compilation termination?

Answer 2

वहाँ एक क्लासिक, कुछ हद तक खतरनाक उदाहरण this paper from 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 

whi की आवश्यकता है च, दिए गए उदाहरण के अनुसार, हम कर सकते हैं। बेशक, हम के लिए कुछ z ऐसे y ~ [z] रखना चाहिए

instance Mul x y z 

अर्थात

instance Mul x [z] z 

कि और हम एक पाश में कर रहे हैं।

यह परेशान है, क्योंकि है कि Mul उदाहरण लगता है कि इसके प्रत्यावर्तन संरचना की दृष्टि से , को कम करने पेट्र के जवाब में स्पष्ट रूप से रोग उदाहरण के विपरीत है। फिर भी यह जीएचसी पाश बनाता है (लटकने से बचने के लिए बोरडम थ्रेसहोल्ड लात मारने के साथ)।

मुसीबत, के रूप में मुझे यकीन है कि मैं कहीं somewhen उल्लेख किया है हूँ, कि पहचान y ~ [z] इस तथ्य के बावजूद किया जाता है कि zy पर कार्यात्मक निर्भर करता है। यदि हम कार्यात्मक निर्भरता के लिए एक कार्यात्मक नोटेशन का उपयोग करते हैं, तो हम देख सकते हैं कि बाधा y ~ Mul x [y] कहती है और घटना जांच को उल्लंघन के रूप में प्रतिस्थापन को अस्वीकार करती है।

Intrigued, मैंने सोचा कि मैं इस एक बार आज़माएंगे चाहते हैं,

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 अक्षम होने के साथ, उदाहरण अभी भी स्वीकार किया गया है और टाइपशेकर अभी भी लूप है, लेकिन कटऑफ बहुत तेज़ी से होता है।

तो ... अजीब पुरानी दुनिया।