haskell - अंतर्ज्ञानवादी सिद्धांत के समकक्ष संयोजक तर्क क्या है?




types functional-programming (2)

मैंने हाल ही में एक विश्वविद्यालय पाठ्यक्रम पूरा किया जिसमें हास्केल और आगादा (एक निर्भर टाइप की गई कार्यात्मक प्रोग्रामिंग भाषा) शामिल थी, और यह सोच रहा था कि संयोजन में लैम्बडा कैलकुस को प्रतिस्थापित करना संभव था या नहीं। हास्केल के साथ यह एस और के संयोजकों का उपयोग करके संभव लगता है, इस प्रकार इसे पॉइंट-फ्री बनाते हैं। मैं सोच रहा था कि एग्डा के बराबर क्या था। हां, क्या कोई भी किसी भी चर का उपयोग किये बिना एग्डा के समतुल्य रूप से टाइप की गई कार्यात्मक प्रोग्रामिंग भाषा बना सकता है?

साथ ही, क्या किसी भी तरह से संयोजकों के साथ मात्रा को प्रतिस्थापित करना संभव है? मुझे नहीं पता कि यह एक संयोग है लेकिन उदाहरण के लिए सार्वभौमिक मात्रा एक प्रकार का हस्ताक्षर लम्बा अभिव्यक्ति की तरह दिखती है। क्या इसका अर्थ बदलने के बिना एक प्रकार के हस्ताक्षर से सार्वभौमिक मात्रा को हटाने का कोई तरीका है? जैसे में:

forall a : Int -> a < 0 -> a + a < a

क्या एक ही चीज़ का उपयोग किए बिना व्यक्त किया जा सकता है?


तो मैंने इसके बारे में कुछ और सोचा और कुछ प्रगति की। यहां मार्टिन-लॉफ के एन्कोडिंग पर एक पहला स्टैब है जो बेहद सरल (लेकिन असंगत) Set : Set एक संयोजक शैली में सिस्टम Set : Set । यह खत्म करने का एक अच्छा तरीका नहीं है, लेकिन यह शुरू करने का सबसे आसान स्थान है। इस प्रकार के सिद्धांत का सिंटैक्स सिर्फ प्रकार के एनोटेशन, पीआई-प्रकार और ब्रह्मांड सेट के साथ लैम्ब्डा-कैलकुलेशन है।

लक्ष्य प्रकार सिद्धांत

पूर्णता के लिए, मैं नियम प्रस्तुत करूंगा। संदर्भ वैधता केवल कहती है कि आप Set एस में रहने वाले ताजा चर के आस-पास के संदर्भों से रिक्त स्थान बना सकते हैं।

                     G |- valid   G |- S : Set
--------------     ----------------------------- x fresh for G
  . |- valid         G, x:S |- valid

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

  G |- valid             G |- S : Set   G |- T : Pi S \ x:S -> Set
------------------     ---------------------------------------------
  G |- Set : Set         G |- Pi S T : Set

  G |- S : Set   G, x:S |- t : T x         G |- f : Pi S T   G |- s : S
------------------------------------     --------------------------------
  G |- \ x:S -> t : Pi S T                 G |- f s : T s

  G |- valid                  G |- s : S   G |- T : Set
-------------- x:S in G     ----------------------------- S ={beta} T
  G |- x : S                  G |- s : T

मूल से एक छोटी भिन्नता में, मैंने लैम्ब्डा को केवल बाध्यकारी ऑपरेटर बनाया है, इसलिए पीआई का दूसरा तर्क एक फ़ंक्शन कंप्यूटिंग होना चाहिए जिस तरह वापसी प्रकार इनपुट पर निर्भर करता है। सम्मेलन द्वारा (उदाहरण के लिए आगाडा में, लेकिन दुख की बात है हास्केल में नहीं), लैम्ब्डा का दायरा जहां तक ​​संभव हो सके आगे बढ़ता है, इसलिए जब आप एक उच्च-आदेश ऑपरेटर का अंतिम तर्क होते हैं तो आप अकसर अबाधित हो सकते हैं: आप देख सकते हैं कि मैंने किया कि पी के साथ। आपका एग्डा प्रकार (x : S) -> T Pi S \ x:S -> T बन जाता है।

( डिग्रेसियनलैम्बडा पर एनोटेशन टाइप करें यदि आप अबास्ट्रक्शंस के प्रकार को संश्लेषित करने में सक्षम होना चाहते हैं। यदि आप अपने मॉडस ऑपरंदी के रूप में जांचने के लिए स्विच करते हैं, तो आपको अभी भी बीटा-रेडेक्स की जांच करने के लिए एनोटेशन की आवश्यकता है (\ x -> t) s , क्योंकि आपके पास पूरे हिस्सों के प्रकारों का अनुमान लगाने का कोई तरीका नहीं है। मैं आधुनिक डिजाइनरों को प्रकारों की जांच करने और बहुत वाक्यविन्यास से बीटा-रेडेक्स को बाहर करने की सलाह देता हूं।)

( डिग्रेशन । यह प्रणाली असंगत है क्योंकि Set:Set विभिन्न प्रकार के "झूठे विरोधाभासों" के एन्कोडिंग की अनुमति देता है। जब मार्टिन-लोफ ने इस सिद्धांत का प्रस्ताव दिया, तो गिरार्ड ने उन्हें अपने स्वयं के असंगत सिस्टम यू में एन्कोडिंग भेजा। इसके बाद के विरोधाभास हर्केंस सबसे स्वच्छ जहरीले निर्माण है जो हम जानते हैं।)

कॉम्बिनेटर सिंटेक्स और सामान्यीकरण

किसी भी तरह, हमारे पास दो अतिरिक्त प्रतीकों, पीआई और सेट हैं, इसलिए हम शायद एस, के और दो अतिरिक्त प्रतीकों के साथ एक संयोजन अनुवाद का प्रबंधन कर सकते हैं: मैंने ब्रह्मांड के लिए यू और उत्पाद के लिए पी चुना है।

अब हम untyped combinatory वाक्यविन्यास (मुक्त चर के साथ) परिभाषित कर सकते हैं:

data SKUP = S | K | U | P deriving (Show, Eq)

data Unty a
  = C SKUP
  | Unty a :. Unty a
  | V a
  deriving (Functor, Eq)
infixl 4 :.

ध्यान दें कि मैंने इस वाक्यविन्यास में टाइप किए गए मुक्त चर शामिल करने के साधन शामिल किए हैं। मेरे हिस्से पर एक प्रतिबिंब होने के अलावा (नाम के योग्य प्रत्येक वाक्यविन्यास एक एम्बेडेड वैरिएबल और >>= perfoming प्रतिस्थापन के साथ एक मुफ्त मोनैड है), यह बाध्यकारी शर्तों के साथ शब्दों को परिवर्तित करने की प्रक्रिया में मध्यवर्ती चरणों का प्रतिनिधित्व करने के लिए आसान होगा संयोजन फार्म

यहां सामान्यीकरण है:

norm :: Unty a -> Unty a
norm (f :. a)  = norm f $. a
norm c         = c

($.) :: Unty a -> Unty a -> Unty a        -- requires first arg in normal form
C S :. f :. a $. g  = f $. g $. (a :. g)  -- S f a g = f g (a g)   share environment
C K :. a $. g       = a                   -- K a g = a             drop environment
n $. g              = n :. norm g         -- guarantees output in normal form
infixl 4 $.

(पाठक के लिए एक अभ्यास सामान्य प्रकार के लिए एक प्रकार को परिभाषित करना और इन परिचालनों के प्रकार को तेज करना है।)

प्रतिनिधित्व सिद्धांत सिद्धांत

अब हम अपने प्रकार के सिद्धांत के लिए एक वाक्यविन्यास परिभाषित कर सकते हैं।

data Tm a
  = Var a
  | Lam (Tm a) (Tm (Su a))    -- Lam is the only place where binding happens
  | Tm a :$ Tm a
  | Pi (Tm a) (Tm a)          -- the second arg of Pi is a function computing a Set
  | Set
  deriving (Show, Functor)
infixl 4 :$

data Ze
magic :: Ze -> a
magic x = x `seq` error "Tragic!"

data Su a = Ze | Su a deriving (Show, Functor, Eq)

मैं बेलेगर्डे और हुक तरीके से एक ब्रुज़िन इंडेक्स प्रतिनिधित्व का उपयोग करता हूं (जैसा कि बर्ड और पैटरसन द्वारा लोकप्रिय है)। टाइप Su a मुकाबले एक और तत्व है, और हम इसे बाइंडर के तहत फ्री वैरिएबल के प्रकार के रूप में उपयोग करते हैं, Ze साथ नए बाध्य चर के रूप में और Su x पुराने फ्री वैरिएबल x का स्थानांतरित प्रतिनिधित्व होता है।

कॉम्बिनेटर्स को शर्तों का अनुवाद करना

और इसके साथ ही, हम ब्रैकेट अबास्ट्रक्शन के आधार पर सामान्य अनुवाद प्राप्त करते हैं।

tm :: Tm a -> Unty a
tm (Var a)    = V a
tm (Lam _ b)  = bra (tm b)
tm (f :$ a)   = tm f :. tm a
tm (Pi a b)   = C P :. tm a :. tm b
tm Set        = C U

bra :: Unty (Su a) -> Unty a               -- binds a variable, building a function
bra (V Ze)      = C S :. C K :. C K        -- the variable itself yields the identity
bra (V (Su x))  = C K :. V x               -- free variables become constants
bra (C c)       = C K :. C c               -- combinators become constant
bra (f :. a)    = C S :. bra f :. bra a    -- S is exactly lifted application

कॉम्बिनेटर्स टाइपिंग

अनुवाद हम जिस तरह से संयोजकों का उपयोग करते हैं, दिखाता है, जो हमें उनके प्रकारों के बारे में काफी सुराग देता है। U और P बस कन्स्ट्रक्टर सेट हैं, इसलिए, अप्रतिबंधित प्रकार लिखना और P लिए "आगाडा नोटेशन" की अनुमति देना, हमारे पास होना चाहिए

U : Set
P : (A : Set) -> (B : (a : A) -> Set) -> Set

K संयोजक का उपयोग कुछ प्रकार के A मूल्य को किसी अन्य प्रकार के G पर निरंतर कार्य करने के लिए किया जाता है।

  G : Set   A : Set
-------------------------------
  K : (a : A) -> (g : G) -> A

S संयोजक का उपयोग एक प्रकार के अनुप्रयोगों को उठाने के लिए किया जाता है, जिस पर सभी भाग निर्भर हो सकते हैं।

  G : Set
  A : (g : G) -> Set
  B : (g : G) -> (a : A g) -> Set
----------------------------------------------------
  S : (f : (g : G) ->    (a : A g) -> B g a   ) ->
      (a : (g : G) ->    A g                  ) ->
           (g : G) ->    B g (a g)

यदि आप S के प्रकार को देखते हैं, तो आप देखेंगे कि यह टाइप सिद्धांत के संदर्भित अनुप्रयोग नियम को बिल्कुल बताता है, इसलिए यह एप्लिकेशन निर्माण को प्रतिबिंबित करने के लिए उपयुक्त बनाता है। यह उसका काम है!

तब हमारे पास केवल बंद चीजों के लिए आवेदन है

  f : Pi A B
  a : A
--------------
  f a : B a

लेकिन एक झगड़ा है। मैंने संयोजक प्रकार के सिद्धांतों को सामान्य प्रकार सिद्धांत में लिखा है, न कि संयोजक प्रकार सिद्धांत। सौभाग्य से, मेरे पास एक मशीन है जो अनुवाद करेगी।

एक कॉम्बिनेटरी टाइप सिस्टम

---------
  U : U

---------------------------------------------------------
  P : PU(S(S(KP)(S(S(KP)(SKK))(S(KK)(KU))))(S(KK)(KU)))

  G : U
  A : U
-----------------------------------------
  K : P[A](S(S(KP)(K[G]))(S(KK)(K[A])))

  G : U
  A : P[G](KU)
  B : P[G](S(S(KP)(S(K[A])(SKK)))(S(KK)(KU)))
--------------------------------------------------------------------------------------
  S : P(P[G](S(S(KP)(S(K[A])(SKK)))(S(S(KS)(S(S(KS)(S(KK)(K[B])))(S(KK)(SKK))))
      (S(S(KS)(KK))(KK)))))(S(S(KP)(S(S(KP)(K[G]))(S(S(KS)(S(KK)(K[A])))
      (S(S(KS)(KK))(KK)))))(S(S(KS)(S(S(KS)(S(KK)(KP)))(S(KK)(K[G]))))
      (S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(S(KS)(S(KK)(KS)))
      (S(S(KS)(S(KK)(KK)))(S(KK)(K[B])))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(KK)(KK))))
      (S(KK)(KK))))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(S(KS)(S(KK)(KK)))
      (S(S(KS)(KK))(KK)))))(S(S(KS)(S(S(KS)(S(KK)(KS)))(S(KK)(KK))))(S(KK)(KK)))))))

  M : A   B : U
----------------- A ={norm} B
  M : B

तो वहां आपके पास यह सब अपठनीय महिमा में है: Set:Set की एक संयोजक प्रस्तुति Set:Set !

अभी भी एक समस्या है। सिस्टम का सिंटैक्स आपको S लिए G , A और B पैरामीटर और इसी तरह के शब्दों के अनुमान लगाने का कोई तरीका नहीं देता है। इसके अनुरूप, हम टाइपिंग व्युत्पन्न एल्गोरिदमिक रूप से सत्यापित कर सकते हैं, लेकिन हम केवल मूल प्रणाली के साथ संयोजक शब्दों को टाइप नहीं कर सकते हैं। एस और के उपयोग पर टाइप एनोटेशन सहन करने के लिए टाइपशेकर को इनपुट की आवश्यकता होती है, प्रभावी ढंग से व्युत्पन्न रिकॉर्डिंग करना। लेकिन यह कीड़े का एक और कर सकते हैं ...

यदि आप शुरू करने के लिए उत्सुक हैं तो यह रोकने के लिए एक अच्छी जगह है। शेष "दृश्यों के पीछे" सामान है।

कॉम्बिनेटर्स के प्रकार उत्पन्न करना

मैंने संबंधित प्रकार सिद्धांत शर्तों से ब्रैकेट अबास्ट्रक्शन अनुवाद का उपयोग करके उन संयोजन प्रकारों को उत्पन्न किया। यह दिखाने के लिए कि मैंने यह कैसे किया, और यह पोस्ट पूरी तरह से व्यर्थ नहीं है, मुझे अपने उपकरण की पेशकश करने दें।

मैं संयोजकों के प्रकार लिख सकता हूं, जो उनके पैरामीटर पर पूरी तरह से सारणीबद्ध हैं। मैं अपने आसान pil फ़ंक्शन का उपयोग करता हूं, जो डोमेन प्रकार को दोहराने से बचने के लिए पीआई और लैम्ब्डा को जोड़ता है, और बदले में मुझे चर से बांधने के लिए हास्केल की फ़ंक्शन स्पेस का उपयोग करने की अनुमति देता है। शायद आप लगभग निम्नलिखित पढ़ सकते हैं!

pTy :: Tm a
pTy = fmap magic $
  pil Set $ \ _A -> pil (pil _A $ \ _ -> Set) $ \ _B -> Set

kTy :: Tm a
kTy = fmap magic $
  pil Set $ \ _G -> pil Set $ \ _A -> pil _A $ \ a -> pil _G $ \ g -> _A

sTy :: Tm a
sTy = fmap magic $
  pil Set $ \ _G ->
  pil (pil _G $ \ g -> Set) $ \ _A ->
  pil (pil _G $ \ g -> pil (_A :$ g) $ \ _ -> Set) $ \ _B ->
  pil (pil _G $ \ g -> pil (_A :$ g) $ \ a -> _B :$ g :$ a) $ \ f ->
  pil (pil _G $ \ g -> _A :$ g) $ \ a ->
  pil _G $ \ g -> _B :$ g :$ (a :$ g)

इन परिभाषित के साथ, मैंने प्रासंगिक खुले उपभेदों को निकाला और अनुवाद के माध्यम से उन्हें चलाया।

एक डी Bruijn एन्कोडिंग टूलकिट

यहां pil बनाने का तरीका बताया गया है। सबसे पहले, मैं Fin इट सेट की एक श्रेणी को परिभाषित करता हूं, जो चर के लिए उपयोग किया जाता है। इस तरह के प्रत्येक सेट में उपरोक्त सेट में एक कन्स्ट्रक्टर-संरक्षित emb एडिंग है, साथ ही एक नया top तत्व भी है, और आप उन्हें अलग बता सकते हैं: embd फ़ंक्शन आपको बताता है कि क्या मूल्य emb की छवि में है।

class Fin x where
  top :: Su x
  emb :: x -> Su x
  embd :: Su x -> Maybe x

हम ज़ाहिर है, Ze और Suc लिए Fin को तुरंत चालू कर सकते हैं

instance Fin Ze where
  top = Ze              -- Ze is the only, so the highest
  emb = magic
  embd _ = Nothing      -- there was nothing to embed

instance Fin x => Fin (Su x) where
  top = Su top          -- the highest is one higher
  emb Ze     = Ze            -- emb preserves Ze
  emb (Su x) = Su (emb x)    -- and Su
  embd Ze      = Just Ze           -- Ze is definitely embedded
  embd (Su x)  = fmap Su (embd x)  -- otherwise, wait and see

अब मैं एक कमजोर ऑपरेशन के साथ कम या बराबर परिभाषित कर सकता हूं।

class (Fin x, Fin y) => Le x y where
  wk :: x -> y

wk फ़ंक्शन को x तत्वों को y के सबसे बड़े तत्वों के रूप में एम्बेड करना चाहिए, ताकि y में अतिरिक्त चीजें कम हों, और इस प्रकार ब्रुज़िन इंडेक्स शब्दों में, अधिक स्थानीय रूप से बाध्य हो।

instance Fin y => Le Ze y where
  wk = magic    -- nothing to embed

instance Le x y => Le (Su x) (Su y) where
  wk x = case embd x of
    Nothing  -> top          -- top maps to top
    Just y   -> emb (wk y)   -- embedded gets weakened and embedded

और एक बार जब आप इसे हल कर लेते हैं, तो रैंक-एन स्कुलल्डगरी का थोड़ा सा बाकी होता है।

lam :: forall x. Tm x -> ((forall y. Le (Su x) y => Tm y) -> Tm (Su x)) -> Tm x
lam s f = Lam s (f (Var (wk (Ze :: Su x))))
pil :: forall x. Tm x -> ((forall y . Le (Su x) y => Tm y) -> Tm (Su x)) -> Tm x
pil s f = Pi s (lam s f)

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


मुझे लगता है कि "ब्रैकेट एब्स्ट्रक्शन" कुछ परिस्थितियों में निर्भर प्रकारों के लिए भी काम करता है। निम्नलिखित पेपर की धारा 5 में आपको कुछ के और एस प्रकार मिलते हैं:

अपमानजनक लेकिन अर्थपूर्ण संयोग
आश्रित प्रकार-सुरक्षित वाक्यविन्यास और मूल्यांकन
कॉनोर मैकब्राइड, स्ट्रैथक्लाइड विश्वविद्यालय, 2010

एक लैम्ब्डा अभिव्यक्ति को एक संयोजक अभिव्यक्ति में कनवर्ट करना मोटे तौर पर एक प्राकृतिक कटौती प्रमाण को हिल्बर्ट स्टाइल सबूत में परिवर्तित करने के अनुरूप होता है।





agda