प्रकार परिवार उदाहरण सबूत संभव हैं?

Question

सबसे पहले, मैंने कुछ सामान्य प्रकार-स्तर प्राकृतिक संख्या सामग्री के साथ शुरू किया।

{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeFamilies #-} 

data Nat = Z | S Nat 

type family Plus (n :: Nat) (m :: Nat) :: Nat 
type instance Plus Z m = m 
type instance Plus (S n) m = S (Plus n m) 

तो मैं एक एन-आयामी ग्रिड का प्रतिनिधित्व करने वाला डेटा प्रकार बनाना चाहता था। (क्या Evaluating cellular automata is comonadic में पाया जाता है की एक सामान्यीकरण।)

data U (n :: Nat) x where 
    Point  :: x       -> U Z  x 
    Dimension :: [U n x] -> U n x -> [U n x] -> U (S n) x 

विचार है कि प्रकार U num xx रों की एक num आयामी ग्रिड, जो "केंद्रित" ग्रिड में एक खास बिंदु पर है के प्रकार है ।

तो मैं इस एक comonad बनाना चाहते थे, और मैंने देखा है यह संभावित रूप से उपयोगी समारोह है कि वहाँ मैं कर सकते हैं:

ufold :: (x -> U m r) -> U n x -> U (Plus n m) r 
ufold f (Point x) = f x 
ufold f (Dimension ls mid rs) = 
    Dimension (map (ufold f) ls) (ufold f mid) (map (ufold f) rs) 

अब हम लागू कर सकते हैं एक "आयाम में शामिल होने के" इस बात का एक n आयामी ग्रिड बदल जाता है इस संयोजक के मामले में एम (आयामी ग्रिड) (एन + एम) - आयामी ग्रिड। cojoin के परिणाम से निपटने पर यह काम में आ जाएगा जो ग्रिड के ग्रिड का उत्पादन करेगा।

dimJoin :: U n (U m x) -> U (Plus n m) x 
dimJoin = ufold id 

अब तक इतना अच्छा है। मैंने यह भी देखा कि Functor उदाहरण ufold के संदर्भ में लिखा जा सकता है।

instance Functor (U n) where 
    fmap f = ufold (\x -> Point (f x)) 

हालांकि, यह एक प्रकार की त्रुटि में परिणाम देता है।

Couldn't match type `n' with `Plus n 'Z' 

लेकिन अगर हम कुछ कॉपी पास्ता को चाबुक करते हैं, तो प्रकार त्रुटि दूर हो जाती है।

instance Functor (U n) where 
    fmap f (Point x) = Point (f x) 
    fmap f (Dimension ls mid rs) = 
    Dimension (map (fmap f) ls) (fmap f mid) (map (fmap f) rs) 

खैर मुझे कॉपी पास्ता के स्वाद से नफरत है, इसलिए मेरा सवाल यह है। मैं टाइप सिस्टम को कैसे बता सकता हूं कि Plus n Zn के बराबर है? और पकड़ यह है: आप परिवार के उदाहरणों में बदलाव नहीं कर सकते हैं जो dimJoin को इसी प्रकार की त्रुटि उत्पन्न करने का कारण बनेंगे। आप अपने प्रकार के बारे में मनमाने ढंग से चीजों को साबित और Refl पर मिलान पैटर्न द्वारा स्थानीय रूप से दायरे में है कि ज्ञान लाने के लिए

{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE PolyKinds #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE TypeOperators #-} 

data Nat = Z | S Nat 

type family Plus (n :: Nat) (m :: Nat) :: Nat 
type instance Plus Z m = m 
type instance Plus (S n) m = S (Plus n m) 

data (:=) :: k -> k -> * where 
    Refl :: a := a 

data Natural (n :: Nat) where 
    Zero :: Natural Z 
    Suc :: Natural n -> Natural (S n) 

plusZero :: Natural n -> n := (n `Plus` Z) 
plusZero Zero = Refl 
plusZero (Suc n) | Refl <- plusZero n = Refl 

यह अनुमति देता है:

Answer 1

आप क्या जरूरत है एक अच्छा प्रोपोज़िशनल समानता प्रकार है।

एक कष्टप्रद बात यह है कि मेरा plusZero सबूत प्राकृतिक प्रश्न पर प्रेरण की आवश्यकता है, जिसे आप डिफ़ॉल्ट रूप से करने में सक्षम नहीं होंगे (क्योंकि यह रनटाइम पर मौजूद नहीं है)। Natural गवाहों के निर्माण के लिए एक टाइपक्लास आसान होगा, हालांकि।

आपके विशेष मामले के लिए एक और विकल्प केवल अपनी टाइप परिभाषा में तर्कों को उलटा करने के लिए हो सकता है ताकि आपको बाईं ओर Z मिल जाए और यह स्वचालित रूप से कम हो जाए। यह सुनिश्चित करने के लिए अक्सर एक अच्छा पहला कदम होता है कि आपके प्रकार उतने सरल होते हैं जितना आप उन्हें बना सकते हैं, लेकिन फिर आपको अधिक जटिल चीजों के लिए प्रायः समानता की समानता की आवश्यकता होगी, भले ही।