Type system notation को कैसे पढ़ें?

 (langdev.stackexchange.com)
1 पॉइंट द्वारा GN⁺ 2023-08-17 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • type system notation अलग-अलग स्रोतों में भले अलग दिखे, लेकिन अगर grammar, typing relation, और inference rules का साझा ढांचा समझ लिया जाए, तो ज़्यादातर रूपांतरों को समझा जा सकता है
  • type system भाषा के abstract syntax पर काम करता है, इसलिए पहले type रखने वाले term और type स्वयं को grammar में अलग करना ज़रूरी है
  • ⊢ e: τ एक typing judgment है, जिसका अर्थ है “expression e का type τ है”, और इसे ऐसे inference rule की तरह पढ़ा जाता है जहाँ क्षैतिज रेखा के ऊपर की सभी शर्तें सही हों तो नीचे का निष्कर्ष भी सही होता है
  • जब variables और functions आते हैं, तो Γ ⊢ e: τ की तरह एक context जुड़ जाता है जो मौजूदा scope में variable names और types को track करता है
  • कई typing rules को recursive type-checking function की तरह पढ़ा जा सकता है, लेकिन हर logical judgment सीधे निर्णययोग्य type-checking algorithm नहीं बन जाता

grammar से शुरू होने वाली type system notation

  • type system एक programming language का syntactic system है, यानी यह भाषा के abstract syntax पर काम करने वाले rules का एक सेट है
  • type system का व्यापक विवरण आम तौर पर पहले उस syntax structure को grammar के रूप में देता है, और फिर उसे BNF notation में लिखता है
  • सबसे सरल type language में भी syntax मोटे तौर पर दो श्रेणियों में बँटा होता है
    • e: type रखने वाले expression
    • τ: expressions पर लगने वाले type
  • उदाहरण भाषा में boolean literals, integer literals, conditional expressions, arithmetic operations, और comparison operations expressions के रूप में होते हैं, और Bool तथा Int types के रूप में इस्तेमाल होते हैं
  • type symbols अलग-अलग स्रोतों में τ की जगह t, T, σ, या दूसरे lowercase Greek letters से भी लिखे जा सकते हैं, लेकिन कुल structure लगभग वही रहता है
  • ज़्यादा जटिल भाषाओं में statements, pattern matching patterns जैसी और भी syntax categories शामिल हो सकती हैं

typing relation और judgment को पढ़ना

  • grammar तय करने के बाद आम तौर पर e : τ के रूप में typing relation परिभाषित की जाती है
    • 1 + 2 : Int का मतलब है “1 + 2 का type Int है”
    • 1 + 2 : Bool का मतलब होगा कि वही expression Bool type का है, जो सही नहीं है
    • true + 2 : Int में expression ही अर्थपूर्ण नहीं है, इसलिए उसका कोई type नहीं बनता
  • ⊢ e : τ एक typing judgment है, और ⊢ को “इसके बाद का कथन सत्य है” की तरह पढ़ा जा सकता है
  • जिन rules में क्षैतिज रेखा के ऊपर कुछ नहीं होता, वे हमेशा सत्य रहने वाले axioms होते हैं
    • ⊢ true : Bool
    • ⊢ false : Bool
    • integer literals के rules जैसे ⊢ 0 : Int, ⊢ 1 : Int, ⊢ -1 : Int
  • जिन rules में ऊपर और नीचे दोनों हिस्से होते हैं, वे inference rules होते हैं
    • अगर ऊपर की सभी शर्तें सत्य हैं, तो नीचे का निष्कर्ष सत्य है
    • अगर e₁ और e₂ दोनों Int हैं, तो e₁ + e₂ का type Int है
    • अगर e₁ और e₂ दोनों Int हैं, तो e₁ < e₂ का type Bool है

conditional expressions और type variables

  • if ... then ... else ... की दोनों branches किसी भी type की हो सकती हैं, लेकिन दोनों का type एक जैसा होना चाहिए
    • if true then 1 else 2 मान्य है
    • if true then false else true मान्य है
    • if true then 1 else true मान्य नहीं है
  • इसे व्यक्त करने के लिए rule branch type दिखाने वाले variable τ का उपयोग करता है
    • condition expression e₁ का type Bool होना चाहिए
    • then branch e₂ और else branch e₃ दोनों का type वही τ होना चाहिए
    • पूरे conditional expression का type भी τ ही होगा
  • rule लागू करते समय τ के लिए कोई भी type चुना जा सकता है, लेकिन उसी rule के अंदर उस चुनाव को एकसमान रखना पड़ता है

inference rules को algorithm की तरह पढ़ना

  • यह notation formal logic से आया है, और type system specification का तरीका खास तौर पर natural deduction से मिलता-जुलता है
  • ऐसे rules का उपयोग system properties के formal proofs बनाने में होता है, और type safety जैसी विशेषताओं को साबित करने में यह महत्वपूर्ण हैं
  • हर logical judgment सीधे किसी निर्णययोग्य type-checking algorithm के बराबर नहीं होता
  • कई मामलों में ⊢ e : τ को ऐसे function की तरह पढ़ा जा सकता है जो expression e से type τ निकालता है
    • grammar में expression के हर form के लिए आम तौर पर एक rule होता है
    • हर typing rule को recursive type-checking function की एक branch की तरह देखा जा सकता है
  • उदाहरण का infer function इस flow से मेल खाता है
    • true या false का type Bool है
    • integer literals का type Int है
    • e₁ + e₂ के लिए पहले देखा जाता है कि दोनों तरफ inference result Int है या नहीं, फिर Int लौटाया जाता है
    • e₁ < e₂ के लिए पहले जाँचा जाता है कि दोनों Int हैं या नहीं, फिर Bool लौटाया जाता है
    • if e₁ then e₂ else e₃ में पहले condition के Bool होने की जाँच होती है, फिर दोनों branches के type एक जैसे हैं या नहीं, और उसके बाद वही type लौटाया जाता है
  • भले इसे सीधे algorithm में न बदला जा सके, judgment में e को input और τ को output की तरह सोचना information flow समझने में मदद करता है

variables और context

  • उपयोगी programming languages को संभालने के लिए variables चाहिए होते हैं, और उदाहरण में functions जोड़कर इसे simply typed lambda calculus के रूप में बढ़ाया जाता है
  • विस्तारित grammar में ये शामिल होते हैं
    • variable x
    • function abstraction λx:τ. e
    • function application e e
    • function type τ → τ
  • λx:τ. e TypeScript के (x:τ) => e के बराबर है, और f x का संबंध f(x) से है
  • variable का type उस context पर निर्भर करता है जहाँ वह आता है, इसलिए सिर्फ ⊢ x : ??? के रूप में rule नहीं लिखा जा सकता
  • इसलिए typing judgment को बढ़ाकर Γ ⊢ e : τ किया जाता है
    • Γ context या type environment है
    • ⊢ बाईं तरफ की context assumptions और दाईं तरफ साबित किए जाने वाले कथन को अलग करता है
    • इसे “context Γ के तहत expression e का type τ है” की तरह पढ़ा जाता है
  • algorithmic नज़रिए से Γ को Map<Variable, Type> जैसे अतिरिक्त input की तरह देखा जा सकता है
  • formal रूप में context को भी syntax structure के रूप में लिखा जाता है
    • ∅: empty context
    • Γ, x:τ: variable binding जोड़ने वाला context
    • कभी-कभी ∅ की जगह • को empty context के रूप में लिखा जाता है
  • इस notation में context, variable names को types से map करने वाली association list के काफ़ी करीब होता है

rules के अंदर context क्या करता है

  • कई typing rules context को बदले बिना वैसे का वैसा आगे बढ़ा देते हैं
    • Γ ⊢ true : Bool
    • अगर Γ ⊢ e₁ : Int और Γ ⊢ e₂ : Int है, तो Γ ⊢ e₁ + e₂ : Int
  • variable use और lambda expression के rules में context की केंद्रीय भूमिका होती है
    • अगर x:τ ∈ Γ है, तो Γ ⊢ x : τ
    • अगर Γ, x:τ₁ ⊢ e : τ₂ है, तो Γ ⊢ (λx:τ₁. e) : τ₁ → τ₂
  • lambda expression के body e की type checking करते समय context को नई binding x:τ₁ से बढ़ाया जाता है
  • variable rule कहता है कि अगर मौजूदा context में variable binding मौजूद है, तो उस variable का वही type माना जाएगा
  • context, lambda rule और variable rule के बीच जानकारी पहुँचाने वाले communication mechanism की तरह काम करता है
  • सरलता के लिए, इस तरह की type system specification आम तौर पर मानती है कि सभी variables पहले से resolve होकर unique बनाए जा चुके हैं, और variable shadowing को नहीं संभालती
  • function application rule function expression और argument expression दोनों के types को साथ में जाँचता है
    • e₁ का type τ₁ → τ₂ होना चाहिए
    • e₂ का type τ₁ होना चाहिए
    • पूरे application e₁ e₂ का type τ₂ होगा

अक्सर दिखने वाली अतिरिक्त notation

  • inference rules हमेशा केवल vertical form में ही नहीं लिखे जाते
    • कई शर्तें horizontal रूप में साथ-साथ रखी जा सकती हैं
    • vertical layout और horizontal layout एक ही rule में मिश्रित भी हो सकते हैं
  • क्षैतिज रेखा के ऊपर की शर्तें आम तौर पर दूसरे judgments होती हैं, लेकिन कोई मनमानी boolean condition, यानी side condition, भी आ सकती है
    • variable rule में x:τ ∈ Γ इसका उदाहरण है
    • algorithmic type systems में α fresh लिखा जा सकता है, जिसका मतलब है कि α एक नया type variable होना चाहिए जो दूसरे type variables से अलग हो

subtyping

  • subtyping types के बीच compatibility को strict equality से थोड़ा ढीले रूप में देखने वाला संबंध है, और इसे स्पष्ट रूप से परिभाषित करना पड़ता है
  • इसे आम तौर पर τ₁ <: τ₂ लिखा जाता है, और पढ़ा जाता है “τ₁, τ₂ का subtype है”
  • एक सरल subtyping relation top type ⊤ और bottom type ⊥ को शामिल कर सकती है
    • τ <: τ: हर type, अपने ही type का subtype है
    • τ <: ⊤: हर type, ⊤ का subtype है
    • ⊥ <: τ: ⊥ हर type का subtype है
  • पहला rule reflexivity rule है, जिसे अक्सर संक्षेप में refl कहा जाता है
  • subtyping की अनुमति देनी हो, तो जिन typing rules में इसकी ज़रूरत है वहाँ इस relation का उपयोग स्पष्ट रूप से दिखाना पड़ता है
    • जैसे function application rule में, अगर argument type τ₁, parameter type τ₂ का subtype है, तो application की अनुमति दी जा सकती है

multiple contexts और bidirectional type checking

  • कुछ type systems ऐसे typing judgments परिभाषित करते हैं जिनमें एक से ज़्यादा contexts होते हैं
    • दूसरे context को आम तौर पर Δ कहा जाता है
    • Γ;Δ ⊢ e : τ अक्सर तब इस्तेमाल होता है जब दोनों contexts input की तरह काम कर रहे हों
    • Γ ⊢ e : τ ⊣ Δ अक्सर तब लिखा जाता है जब Δ output की तरह काम कर रहा हो
  • दूसरे context का उपयोग उसके उद्देश्य के अनुसार बदलता है
    • इसका उपयोग यह सीमित करने के लिए हो सकता है कि कुछ variables को केवल किसी खास expression के अंदर ही refer किया जा सके
    • resource-aware programming languages में यह output context के रूप में track कर सकता है कि कौन-से variables consume हो चुके हैं
  • bidirectional type checking ऐसा तरीका है जो constraint solver के बिना सीमित non-local type inference करता है
  • bidirectional system सामान्य Γ ⊢ e : τ judgment को दो विशेष judgments में बाँट देता है
    • Γ ⊢ e ⇐ τ: यह checking judgment है, जो जाँचता है कि expression e का expected type τ है या नहीं; algorithmic रूप से τ input है
    • Γ ⊢ e ⇒ τ: यह inference judgment है, जो तब इस्तेमाल होता है जब expected type की जानकारी न हो; algorithmic रूप से τ output है
  • दोनों judgments को परस्पर recursive तरीके से परिभाषित किया जाता है ताकि type information दोनों दिशाओं में प्रवाहित हो सके
  • इस तरीके में कुछ type annotations छोड़े जा सकते हैं, और lambda abstraction के checking rule में expected function type से parameter type मिल जाने के कारण variable binder पर annotation छोड़ा जा सकता है

संबंधित पढ़ाई

1 टिप्पणियां

 
GN⁺ 2023-08-17
Hacker News की रायें

  • Guy Steele ने पहले इस विषय पर एक talk दी थी। कुछ notations को उन्होंने खोजे जा सकने वाले नाम भी दिए थे, जैसे दो-आयामी inference-rule diagrams
    वे इसे computer science metanotation कहते हैं, लेकिन निजी तौर पर यह programming language theory के ज़्यादा करीब लगता है। https://m.youtube.com/watch?v=dCuZkaaou0Q

    • Guy Steele के quote की तरह, यह सचमुच अफ़सोस की बात है कि “computer science की सबसे लोकप्रिय programming language” के पास न compiler है, न interpreter, न पूरी specification, और दशकों से बस variants बढ़ते गए हैं
      https://en.wikipedia.org/wiki/Guy_Steele Guy Steele
      https://www.codemesh.io/codemesh2017/guy-l-steele Code Mesh 2017 में "A Cobbler's Child" talk
      https://www.youtube.com/watch?v=qNPlDnX6Mio "A Cobbler's Child" (YouTube पर video)
      https://www.youtube.com/watch?v=dCuZkaaou0Q "It's Time for a New Old Language" (YouTube पर video)
      https://news.ycombinator.com/item?id=15473199 HN पर discussion
      https://labs.oracle.com/pls/apex/f?p=94065:40150:0::::P40150... Slides
      अजीब है कि इंसानी कला-कौशल की सबसे सटीक चीज़ों को सबसे सटीक तरीके से बताने वाले लोग अस्पष्ट और असंगत notation इस्तेमाल कर रहे हैं
    • उस समय भी इस पर बात हुई थी: It's Time for a New Old Language – Guy Steele [video] - https://news.ycombinator.com/item?id=15473199 - Oct 2017 (45 comments)
    • Slides PDF के रूप में नहीं मिल रहीं; जानना चाहूंगा कि क्या वे कहीं upload की गई थीं
    • ऊपर से intro Rich Hickey ने दिया था—काफ़ी दमदार

  • यह notation Frege तक जाती है। अगर पता न हो कि क्या खोजना है, तो इसे खोज पाना मुश्किल है, लेकिन यह लेख काफ़ी अच्छा summary लगता है: https://plato.stanford.edu/entries/frege-logic
    turnstile symbol |- पहले से इस्तेमाल में था, और class में “Fregescher Schlussstrich”, यानी Frege की conclusion stroke कही जाने वाली horizontal line, मूल रूप से turnstile का ही हिस्सा थी और लगता है आधुनिक notation में अलग element बन गई

    • “Schlussstrich” का अनुवाद शायद deduction stroke या inference stroke के ज़्यादा करीब होगा

  • Benjamin C. Pierce की Types and Programming Languages इस तरह की चीज़ों को cover करने वाली अच्छी textbook है

    • irony यह है कि TAPL खुद जिस syntax का इस्तेमाल करती है, उसके basic meaning को समझाने में काफ़ी अस्पष्ट है। यह जवाब TAPL से कई orders of magnitude ज़्यादा स्पष्ट है

  • computer science major होने के बावजूद |– और |= के meaning का difference, और इस्तेमाल हुए variables किस meta-syntax level पर हैं, यह अब भी उलझाता है
    irony यह है कि इसकी एक वजह यह है कि notation में खुद explicit types नहीं हैं

  • जो लोग पढ़ने को लेकर हिचक रहे हैं: यह लेख computer science papers में आने वाली type system notation की explanation है, और असल में type systems के लिए BNF notation, inference rules वगैरह का primer है
    अच्छा summary लगता है

    • सच कहूं तो बस एक cheatsheet चाहिए जो बताए कि symbols को English words में कैसे पढ़ना है
      type application का logical concept समझता हूं, लेकिन computer science papers अक्सर नहीं पढ़ता, इसलिए symbols और meanings का mapping दिमाग में ठीक से बैठता नहीं
    • यह कि ऐसी चीज़ को वर्षों में इतनी अच्छी तरह abstract किया गया है, computer science वाली खासियत दिखाता है

  • examples में 𝗍𝗋𝗎𝖾+2:𝖨𝗇𝗍 का मतलब “𝗍𝗋𝗎𝖾+2 का type 𝖨𝗇𝗍 है” बताया गया है, लेकिन फिर कहा गया है कि expression 𝗍𝗋𝗎𝖾+2 खुद ही nonsensical है और इसका कोई type नहीं, इसलिए यह और अजीब है
    लेकिन Python में True + 2 सच में integer है और उसका value 3 है। ऐसा होना चाहिए या नहीं, यह अलग बात है; असल में ऐसा है

    • अगर आपको लगता है कि True + 2 समझ में आता है, तो बस ऐसा allow करने वाला judgment rule खुद define कर दीजिए
      logic और type system theory को इस बात से फर्क नहीं पड़ता कि आप कौन-से axioms और inference rules इस्तेमाल करते हैं; वे बस आपको उन rules और उनके interactions के बारे में infer करने देते हैं। उदाहरण के लिए |- True : Bool, |- True : Int रख सकते हैं, या अगर सिर्फ specific expressions में allow करना हो तो |- x : Int से |- True + x: Int derive करने जैसा बना सकते हैं
    • क्या यह language-specific नहीं है? जैसे C में true 1 पर map होता है, इसलिए true+1=2 हो जाता है
    • Python या C में True + 2 error न भी दे, तब भी programmers को थोड़ा syntactic sugar देने के लिए language semantics को infer करना मुश्किल बना देता है, इसलिए यह अब भी मूर्खतापूर्ण है

  • अच्छा है। कई सालों से जिज्ञासा थी, लेकिन और जानने के लिए कौन-से search terms डालूं, पता नहीं था

  • कभी-कभी जब कोई मेहनत से सीखी हुई गुप्त विद्या मुफ्त में खोल देता है, तो बेवजह बुरा लगता है ;) जब मैं यह सीख रहा था, तब ऐसा लेख होता तो सच में अच्छा होता। उम्मीद है accessibility बढ़े तो गड़बड़ languages कम हों

  • Ada Reference Manual पढ़ते समय इस तरह के syntax को तुरंत पहचान लिया था। नाम नहीं जानता था, लेकिन असली use case में देखकर दिलचस्प लगा, और पूरी language उसी notation से define की गई है
    उदाहरण: https://ada-lang.io/docs/arm/AA-3/AA-3.7#syntax

    • http://www.ada-auth.org/standards/22rm/html/RM-1-1-4.html
      Ada Reference Manual अपने इस्तेमाल किए गए notation को स्पष्ट करता है। यह Backus-Naur Form का एक variant इस्तेमाल करता है, और link किए गए section में उस खास variant को समझाया गया है

  • लगता है यह उस एक मुद्दे का प्रचार करने के लिए अच्छी जगह है जिस पर मैं अंत तक अड़ा रहने वाला हूँ। colon का इस्तेमाल करने वाले type annotation format में colon के दोनों तरफ spacing समान होनी चाहिए
    मेरे हिसाब से ये संयोग से एक जैसे दिखने वाले—यानी दो dots से बने—दो अलग-अलग symbols हैं। एक label colon है, जैसे English में आगे वाला हिस्सा पीछे वाले को introduce करता है या left side right side का label होता है; Python में block शुरू करना, key-value pair, C या Rust में struct name-value pair इसी में आते हैं
    दूसरा mathematics से लिया गया type annotation है। यह एक binary relation है, और binary relation में left-right spacing समान रखी जाती है। जैसे हम x= 1, x> y, x+ z नहीं लिखते, वैसे ही x: X नहीं बल्कि x : X लिखना natural लगता है
    a: b देखते ही यह तुरंत label colon की तरह पढ़ा जाता है, और अगर वह type annotation हो तो हर बार बहुत छोटा-सा अतिरिक्त mental transformation चाहिए होता है। यह programming language syntax की बात है, और निजी तौर पर मुझे X x की तुलना में x : X कहीं ज्यादा पसंद है
    [1] “Evangelion” εὐαγγέλιον से आया एक शानदार शब्द है, यानी अच्छी खबर। [2] https://en.wikipedia.org/wiki/Colon_(punctuation)#Usage_in_E...

    • कुछ गलतफहमियां हो सकती हैं। mathematics writing में भी f: X->Y जैसी notation सच में मिलती है, जिसमें colon के right में ज्यादा space होता है, और मैंने जिन 3 किताबों को देखा उनमें से 1 ने सिर्फ वही notation इस्तेमाल की थी
      साथ ही वह भी अभी तक labeling के करीब ही है, यानी किसी खास तरह के map को label करना। mathematics में colon सचमुच अलग अर्थ में तब इस्तेमाल होता है जब वह such that का abbreviation होता है; जैसे { x : x \in IN and x | 2} जैसे set definition में या quantifier के साथ यह अक्सर आता है
    • दिलचस्प नजरिया है। अतिरिक्त mental step वाली बात वैसी ही है जैसी मुझे common X x notation पढ़ते समय महसूस होती है। x: X मुझे कहीं ज्यादा natural लगता है, और natural language में colon इस्तेमाल करने के तरीके के भी करीब लगता है
      कोई proposition होता है और colon के बाद वाला हिस्सा उसे ज्यादा detail में समझाता है; type भी left में मौजूद चीज के बारे में अतिरिक्त जानकारी है, इस लिहाज से यह बिल्कुल फिट बैठता है
    • type theory में आम तौर पर t[space]:[space]T की तरह colon के दोनों तरफ समान space रखना standard practice माना जाता है
      type theory कुल मिलाकर असंगतियों से भरी गड़बड़ चीज है, लेकिन यह उन दुर्लभ मामलों में से है जहां सभी काफी consistent हैं। undergraduate में मैंने कैसे लिखा था, यह जानने के लिए देखा तो पाया कि मैंने भी अच्छे से symmetric तरीके से लिखा था: https://dvt.name/logic/horse2.pdf
    • x: X “colon के बाद explanation आती है” वाले usage से match करता है
      यानी variable x: It’s an X. जैसा
    • age: int को English में “person’s age: an integer” की तरह आसानी से पढ़ा जा सकता है
      इसलिए colon मुझे कभी खास परेशान करने वाला नहीं लगा