टाइप कैसे सिद्ध होते हैं — TypeScript टाइप सिस्टम और Curry–Howard correspondence

सारांश:

• यह TypeScript के टाइप सिस्टम को सिर्फ एक static type checker नहीं, बल्कि तर्कशास्त्र की proof system के रूप में समझने का दृष्टिकोण प्रस्तुत करता है।
• Curry–Howard correspondence (Type = Proposition, Program = Proof) के आधार पर यह अवधारणात्मक रूप से समझाता है कि type inference संभव क्यों है।
• function type, generics, conditional type, type narrowing जैसी TypeScript सुविधाओं को logical implication, universal quantification और case analysis से जोड़कर समझाया गया है।
• type check प्रक्रिया को rule application के बजाय propositions के बीच संबंध को सत्यापित करने की प्रक्रिया के रूप में देखा गया है।
• implementation details की बजाय TypeScript टाइप सिस्टम की design background और mathematical structure पर ध्यान केंद्रित किया गया है।

विस्तृत सारांश:

1. पृष्ठभूमि: type inference संभव क्यों है?
   static type languages में type inference को अक्सर इस implementation समस्या के रूप में समझाया जाता है कि “compiler type को कैसे मिलाता है।”
   यह लेख उससे एक कदम पीछे जाकर पूछता है कि type inference मूल रूप से संभव ही क्यों है।
   इसके उत्तर में यह टाइप सिस्टम को तर्कशास्त्र की proof system के रूप में देखने का दृष्टिकोण प्रस्तुत करता है।

2. सैद्धांतिक आधार: Curry–Howard correspondence
   Curry–Howard correspondence के अनुसार type, proposition के अनुरूप होता है और program, उस proposition के proof के अनुरूप होता है।
   इस दृष्टिकोण में type check को इस प्रक्रिया के रूप में समझा जाता है कि program किसी विशेष proposition को संतुष्ट करता है या नहीं।

3. TypeScript फीचर्स और logical structure का correspondence
   लेख में TypeScript की प्रमुख सुविधाओं को इस तरह जोड़ा गया है।

• function type → logical implication
• generics → universal quantification
• conditional type / type narrowing → case analysis
  इसके माध्यम से यह समझाया गया है कि कुछ type expressions स्वाभाविक क्यों लगते हैं,
  और कुछ types को structural रूप से व्यक्त करना कठिन क्यों होता है।

4. टाइप सिस्टम की सीमाएँ और design choices
   इस दृष्टिकोण से TypeScript की बाधाएँ और सीमाएँ “features की कमी” नहीं, बल्कि logical consistency बनाए रखने के लिए किए गए design choices के रूप में समझी जाती हैं।
   लेख व्यावहारिक techniques या tricks से अधिक इस बात पर केंद्रित है कि टाइप सिस्टम किस दर्शन और गणितीय पृष्ठभूमि पर निर्मित हुआ है।

[pjh2568]

बहुत दिलचस्प था, पढ़कर अच्छा लगा। धन्यवाद

[devjeonghwan]

कहा तो यह जाता है कि यह linting नहीं है.. लेकिन अगर यह साबित करना है कि type checking सख्त Contract पालन है, तो क्या उस contract को binary और runtime में enforce नहीं किया जाना चाहिए? अगर ऐसा नहीं है, तो मुझे लगता है कि यह अब भी floating syntax स्तर की type linting ही है।

[tsboard]

यह बहुत प्रभावशाली था। मुझे पहली बार पता चला कि इसे इस नज़रिए से भी देखा जा सकता है। मैंने अपने सहकर्मियों से भी इसे एक बार देखने के लिए कहा और कंपनी में भी ब्लॉग लिंक शेयर किया। धन्यवाद!