मैं नियमित फिक्स्ड-पॉइंट प्रकार संयोजक को समझता हूं और मुझे लगता है कि मैं उच्च-आदेश निश्चित-एन प्रकार संयोजक समझता हूं, लेकिन HFix मुझे बढ़ाता है। क्या आप डेटा-प्रकारों के सेट और उनके (मैन्युअल रूप से व्युत्पन्न) निश्चित बिंदुओं का उदाहरण दे सकते हैं जिन्हें आप HFix पर लागू कर सकते हैं।हास्केल के मल्टीरेक पैकेज में 'HFix` कैसे काम करता है?
प्राकृतिक संदर्भ कागज Generic programming with fixed points for mutually recursive datatypes जहां multirec package समझाया गया है है।
HFix पारस्परिक रूप से रिकर्सिव डेटा प्रकारों के लिए एक फिक्सपॉइंट प्रकार संयोजक है। ,
Fix :: (∗ -> ∗) -> ∗
Fix2 :: (∗ -> ∗ -> ∗) -> (∗ -> ∗ -> ∗) -> ∗
Fixn :: ((∗ ->)^n * ->)^n ∗
≈
Fixn :: (*^n -> *)^n -> *
कितने प्रकार यह एक निश्चित बिंदु पर करता प्रतिबंधित करने के लिए वे: यह अच्छी तरह से पत्र में धारा 3.2 में समझाया गया है, लेकिन यह विचार इस पैटर्न के सामान्यीकरण के है *^n के बजाय टाइप कंस्ट्रक्टर का उपयोग करें। वे एक एएसटी डेटा प्रकार का उदाहरण देते हैं, पेपर में पर पारस्परिक रूप से रिकर्सिव। मैं आपको शायद सबसे सरल उदाहरण प्रदान करता हूं। हमें HFix करते इस डेटा प्रकार:
data Even = Zero | ESucc Odd deriving (Show,Eq)
data Odd = OSucc Even deriving (Show,Eq)
हमें इस डेटाप्रकार के लिए परिवार विशिष्ट GADT परिचय करते हैं के रूप में खंड 4,1
data EO :: * -> * where
E :: EO Even
O :: EO Odd
EO Even में किया जाता है मतलब है कि हम एक सम संख्या चारों ओर ले जाने के कर रहे हैं। हमें इस काम के लिए एल उदाहरणों की आवश्यकता है, जो कहता है कि कौन सा विशिष्ट निर्माता हम EO Even और EO Odd लिखते समय क्रमशः प्रतिक्रिया दे रहे हैं।
instance El EO Even where proof = E
instance El EO Odd where proof = O
ये HFunctor instance I के लिए के लिए बाधाओं के रूप में इस्तेमाल कर रहे हैं।
अब हम पैटर्न और अजीब डेटा प्रकार के लिए पैटर्न मज़ेदार को परिभाषित करते हैं। हम लाइब्रेरी से संयोजकों का उपयोग करते हैं।:>: प्रकार निर्माता टैग अपने प्रकार सूचकांक के साथ एक मूल्य:
type PFEO = U :>: Even -- ≈ Zero ::() -> EO Even
:+: I Odd :>: Even -- ≈ ESucc :: EO Odd -> EO Even
:+: I Even :>: Odd -- ≈ OSucc :: EO Even -> EO Odd
अब हम इस पद्धति functor के आसपास शादी करने HFix उपयोग कर सकते हैं:
type Even' = HFix PFEO Even
type Odd' = HFix PFEO Odd
ये अब भी और ईओ ईओ isomorphic को कर रहे हैं अजीब है, और अगर हम इसे Fam का एक उदाहरण बनाने के हम hfrom and hto functions उपयोग कर सकते हैं:
type instance PF EO = PFEO
instance Fam EO where
from E Zero = L (Tag U)
from E (ESucc o) = R (L (Tag (I (I0 o))))
from O (OSucc e) = R (R (Tag (I (I0 e))))
to E (L (Tag U)) = Zero
to E (R (L (Tag (I (I0 o))))) = ESucc o
to O (R (R (Tag (I (I0 e))))) = OSucc e
एक साधारण छोटे से परीक्षण:
test :: Even'
test = hfrom E (ESucc (OSucc Zero))
test' :: Even
test' = hto E test
*HFix> test'
ESucc (OSucc Zero)
एक बीजगणित उनके Int मूल्य में बदल जाएगा Even और Odd रों के साथ एक और मूर्खतापूर्ण परीक्षण:
newtype Const a b = Const { unConst :: a }
valueAlg :: Algebra EO (Const Int)
valueAlg _ = tag (\U -> Const 0)
& tag (\(I (Const x)) -> Const (succ x))
& tag (\(I (Const x)) -> Const (succ x))
value :: Even -> Int
value = unConst . fold valueAlg E
धन्यवाद, यह पढ़ में मदद मिली है, लेकिन मैं अभी भी कर रहा हूँ थोड़ा सा उलझा हुआ। क्या आप ':>:' पर अधिक विस्तार से जा रहे हैं, यह अभी भी मेरे लिए काफी अपारदर्शी दिखता है। –
हां यह काफी शामिल पुस्तकालय है। मैंने इसके बारे में एक छोटी टिप्पणी दी, अभी अभी और समय नहीं है। चीयर्स! – danr
इसमें थोड़ी देर लग गई, लेकिन इसे पढ़ने और पढ़ने के बाद, एपीआई दस्तावेज़ और पेपर, अंततः यह समझ में आता है। बहुत बहुत धन्यवाद, आपने बहुत मदद की है। –