2016-08-14 13 views
6

कैसे मैं एक forall बाधा उदाहरण के लिए कुछ प्रकार परिवारों F और G के लिए लिख सकता हूँ? और यदि ऐसा हो तो एक छोटा सा उदाहरण प्रदान किया जा सकता है? मुझे लगता है कि मुझे Forall का उपयोग करने की आवश्यकता है।बाधाओं forall

+0

क्या आप इसे एक बड़े प्रकार की बाधा बनने के लिए देख रहे हैं या क्या आप वास्तव में मूल्य समानता चाहते हैं? यह आप जो करने की कोशिश कर रहे हैं उसके बारे में अधिक जानकारी प्रदान करने में मदद कर सकता है। –

+0

यदि आप समानता का प्रतिनिधित्व करने के लिए मूल्य की तलाश में हैं, तो 'समानता वैल :: जी (एफ एक्स वाई): ~: (x, y); समानता वैल = ... रेफ्ल ... ''' type.Equality' से '' ~ ~ '' '' ''। यदि, दूसरी तरफ, यह एक बड़े प्रकार पर बाधा है, क्या आपके पास सिर्फ 'जी (एफ एक्स वाई) ~ (x, y) => ... '? मेरा मानना ​​है कि बाधाओं से 'फोरल' पैकेज सार्वभौमिक रूप से बाधाओं (जैसे कि '(फोरल पी, पीए) => ए') से है, जहां 'पी' तब' न्यू 'जैसी बाधा हो सकती है, जो ऐसा प्रतीत नहीं होता है जो भी आप खोज रहे हैं (यदि मैं सही ढंग से समझ रहा हूं)। –

उत्तर

6

हां, यह constraints का उपयोग कर संभव है। सावधान रहें, हालांकि! आपके द्वारा दावा की जाने वाली समानता constraints के लिए पर्याप्त सामान्यता के साथ पकड़ने की संभावना नहीं है यदि प्रकार परिवार गैर-तुच्छ हैं। विशेष रूप से विचार करें,, चाहे प्रकार परिवारों को सफलतापूर्वक को कम जब x और y अटक प्रकार परिवारों

type family X where {} 
type family Y where {} 

भी कर रहे हैं, मुझे लगता है कि अपने विशेष वांछित बाधा नहीं मुक्त चर जो भी है। उम्मीद है कि यह सिर्फ एक उदाहरण है; इस तरह की एक वास्तविक बंद बाधा उपयोगी होने की संभावना नहीं है।


Data.Constraint.Forall में मौलिक प्रकार परिवार Forall है। ForallT का उपयोग करके यह विशेष उदाहरण थोड़ा और आसानी से संभाला जा सकता है, लेकिन यह समझना सबसे महत्वपूर्ण है कि Forall का उपयोग कैसे करें।

आम तौर पर, Forall p का अर्थ forall x . p x है। यह बहुत सामान्य नहीं लगता है, लेकिन वास्तव में, यदि आप अपना p चरण-दर-चरण तैयार करते हैं। आप

forall x y. G (F x y) ~ (x, y) 

आपके द्वारा प्राप्त रिश्ते को व्यक्त करने वाली कक्षा को परिभाषित करके प्रारंभ करें।

class G (F x y) ~ (x, y) => C x y 
instance G (F x y) ~ (x, y) => C x y 

अब आप चरण दर चरण जा सकते हैं, को परिभाषित करने

class Forall (C x) => D x 
instance Forall (C x) => D x 

और फिर Forall D का उपयोग कर (D x = forall y . C x y के रूप में आप पढ़ सकते हैं), (यानी, forall x . D x) अपने बाधा व्यक्त करते हैं। Dict (D x) प्राप्त करने के लिए आपको inst का उपयोग करने की आवश्यकता होगी और फिर Dict (C x y) प्राप्त करने के लिए।

संबंधित मुद्दे