निर्भर प्रकारों का उपयोग क्यों नहीं किया जाता

• निर्भर प्रकार(type theory) में proof objects शामिल होते हैं, लेकिन लेखक इसे अनावश्यक और अक्षम संरचना मानते हैं
• लेखक ने AUTOMATH और Martin-Löf औपचारिक प्रणाली जैसे पुराने निर्भर-प्रकार आधारित सिस्टमों का सीधे अध्ययन किया, लेकिन Isabelle आगे चलकर सामान्य(generic) logical framework के रूप में विकसित हुआ
• सरल प्रकार सिद्धांत(higher-order logic) पर आधारित Isabelle/HOL, automation, बड़े पैमाने की libraries, और readability में मजबूत है
• ALEXANDRIA project के माध्यम से यह सिद्ध किया गया कि केवल higher-order logic से भी उन्नत गणितीय प्रमेयों का formalization संभव है
• Lean जैसे निर्भर-प्रकार सिस्टम परिपक्व हो जाने के बावजूद, performance issues और complexity के कारण लेखक अब भी higher-order logic approach की व्यावहारिकता को प्राथमिकता देते हैं

---

निर्भर प्रकार और proof objects

• निर्भर प्रकार सिद्धांत में proof objects अनिवार्य हैं, लेकिन लेखक इन्हें स्थान की बर्बादी मानते हैं
  • LCF संरचना में वैध proof steps केवल logic के अंदर नहीं बल्कि implementation language स्तर की type checking के माध्यम से ही चल सकते हैं
  • Robin Milner की अंतर्दृष्टि से proof kernel की अवधारणा आई, जो Isabelle की नींव बनी
• लेखक “आपने निर्भर प्रकारों का उपयोग क्यों नहीं किया?” इस प्रश्न का उत्तर देते हैं: “मैंने बहुत लंबे समय तक किया था”

AUTOMATH का अनुभव

• 1977 में Caltech में लेखक ने N. G. de Bruijn का AUTOMATH व्याख्यान सुना, लेकिन सिस्टम को स्वयं इस्तेमाल नहीं कर पाए
  • उस समय Eindhoven University system ARPAnet से जुड़ा नहीं था, और ALGOL 60 आधारित कंप्यूटर की आवश्यकता थी
• AUTOMATH एक निर्भर-प्रकार सिस्टम है, लेकिन यह Curry–Howard correspondence को लागू नहीं करता
  • उपयोगकर्ता को अपनी इच्छित logic के symbols और inference rules को axioms के रूप में जोड़ना पड़ता था
  • de Bruijn ने इसकी तुलना “ऐसे बड़े रेस्टोरेंट से की जहाँ हर तरह का खाना मिलता है”
• Isabelle ने इसी विचार को आगे बढ़ाते हुए logical framework के रूप में सामान्यता हासिल करने की कोशिश की
  • लेकिन de Bruijn set theory को नापसंद करते थे और गणित को मूलतः type-based मानते थे
• लेखक ने AUTOMATH की soundness verification पर सवाल उठाया, और de Bruijn ने language theory पर 300 पन्नों की किताब भेजी, लेकिन वह संतोषजनक नहीं लगी

Martin-Löf type theory

• Göteborg के Chalmers University में Martin-Löf type theory का अध्ययन करते हुए लेखक program synthesis की संभावना से प्रभावित हुए
  • Heyting की intuitionistic logic के सिद्धांतों को सीधे लागू करने के कारण इसे “सही” दृष्टिकोण माना गया
• कई वर्षों तक शोध जारी रखते हुए लेखक ने Isabelle के शुरुआती संस्करण को Martin-Löf theory में लागू किया
  • यह आज भी Isabelle/CTT के रूप में distribution में शामिल है
• लेकिन Per Martin-Löf केंद्रित कट्टर माहौल और थोपी गई intensional equality की ओर बदलाव ने इस शोधधारा को कमजोर कर दिया
• बाद में आए Calculus of Constructions(CoC), Rocq, Lean आदि ने भी यही सवाल छोड़े
  • CoC में दशकों तक कई variants और optional axioms जोड़े जाते रहे

शोध के विकल्प और Isabelle की दिशा

• शोधकर्ताओं को नई formal systems विकसित करने और मौजूदा systems का विस्तार कर उपयोग करने के बीच चयन करना होता है
  • Isabelle को सामान्यीकृत framework के रूप में डिज़ाइन किया गया, ताकि वह कई तरह की logic को समाहित कर सके
• 1985 में Mike Gordon ने Church की simple type theory से hardware verification किया
  • बाद में John Harrison ने vector dimensions की encoding विकसित की
• Isabelle/HOL ने Church theory में axiomatic type classes और locale module system जोड़ा
• Lean community ने CoC आधारित विशाल गणितीय formalization(mathlib) हासिल किया

ALEXANDRIA project और higher-order logic की सीमाओं की परीक्षा

• ERC समर्थित ALEXANDRIA project ने Isabelle की automation, libraries, और readability पर ज़ोर दिया
• शुरुआत में माना गया था कि higher-order logic की सीमाएँ सामने आएँगी, लेकिन व्यवहार में Grothendieck schemes जैसे उन्नत गणित भी सफलतापूर्वक formalize किए गए
  • Paulo Emílio de Vilhena और Martin Baillon ने सिद्ध किया कि हर field का एक algebraically closed extension होता है
• project आगे बढ़कर Balog–Szemerédi–Gowers theorem जैसे उन्नत परिणामों तक पहुँचा
  • “निर्भर प्रकारों के बिना गणितीय formalization असंभव है” यह दावा गायब हो गया, और केवल “निर्भर प्रकार अधिक साफ-सुथरे हैं” जैसा दावा बचा

Lean और निर्भर प्रकारों पर वर्तमान दृष्टिकोण

• Lean की community size और Blueprint tool ईर्ष्या जगाते हैं, लेकिन performance issues और complexity अब भी बने हुए हैं
  • intensional equality से टकराव और निर्भर प्रकार कब इस्तेमाल करना चाहिए यह तय करने की कठिनाई बार-बार रिपोर्ट की जाती है
• लेखक निर्भर प्रकारों की तुलना Tesla के Full Self-Driving से करते हैं और अत्यधिक उम्मीदों तथा वास्तविक असुविधाओं की ओर इशारा करते हैं

परिशिष्ट: higher-order logic की सैद्धांतिक सीमाएँ

• कुछ लोग दावा करते हैं कि higher-order logic proof-theoretically कमजोर है, लेकिन इसका अर्थ केवल इतना है कि यह ZF set theory की तुलना में कमजोर है
• ALEXANDRIA के परिणामों के अनुसार, higher-order logic से भी Grothendieck schemes जैसी जटिल गणितीय संरचनाओं को संभाला जा सकता है
  • केवल दो proofs में ZF axioms जोड़ने की आवश्यकता पड़ी, और वे भी ऐसे प्रमेय थे जो सीधे ZF objects का उल्लेख करते थे

फुटनोट

• intuitionism एक ऐसी दार्शनिक दृष्टि है जो भाषा को मात्र अभिलेखन का साधन मानती है, और यह आज की constructive mathematics से अलग है

[GN⁺]

Hacker News राय

• dependent types कुछ स्थितियों में बहुत उपयोगी होते हैं
  उदाहरण के लिए, अच्छा होगा अगर Python “10×5 आकार की float32 matrix” को type के रूप में व्यक्त कर सके और type-check कर सके
  लेकिन Curry–Howard correspondence की तरह proof और type को एक मानने की अवधारणा इंसानी नज़रिए से उलझाऊ लगती है
  type error सिर्फ़ एक ऐसी गलती लगती है जिसे ठीक किया जा सकता है, लेकिन proof error कहीं ज़्यादा जटिल होता है और सोच-विचार मांगता है
  इसलिए Lean की असली ताकत type system नहीं, बल्कि community और mathlib की open source संरचना मानी जाती है
  जहाँ Isabelle का AFP किसी academic journal की तरह चलता है, वहीं Lean में pull request-आधारित collaboration बहुत सक्रिय है
  मैं अभी नया theorem prover Acorn(acornprover.org) विकसित कर रहा हूँ, और Lean व Isabelle की खूबियों को मिलाने की कोशिश कर रहा हूँ
  Lean की सरल dependent-type expressiveness अच्छी है, लेकिन इसे बहुत गहराई से इस्तेमाल करने पर debugging कठिन हो जाती है

  • C++ या Rust में भी constant-size arrays के लिए इस तरह का type expression संभव है
    हालाँकि, जो index range सिर्फ runtime पर पता चलती है, उसे compile time पर guarantee नहीं किया जा सकता
    असली dependent-type language runtime errors को type level पर रोक सकती है
  • Rust के const generics या C++ के non-type template parameter से भी यह काफ़ी हद तक संभव है
    वास्तव में dependent-type languages में भी runtime error रोकने के लिए dependent types का उपयोग कम ही होता है,
    इन्हें ज़्यादातर data structure invariants या program definition के बाद verification के लिए इस्तेमाल किया जाता है
    संबंधित संदर्भ: division-by-zero in type theory FAQ, Xavier Leroy प्रस्तुति सामग्री
  • TypeScript में भी dependent types की थोड़ी नकल की जा सकती है
    उदाहरण के लिए, इस code की line 38 की तरह type से matrix का size व्यक्त किया जा सकता है
    vector type definition या
    matrix multiplication result type भी implement किया गया है
    हालाँकि, यह अभी personal project स्तर पर प्रयोग में है और बड़े data projects के लिए उपयुक्त न भी हो
  • “proof type के बराबर है” जैसी अभिव्यक्ति दिलचस्प है
    यह Propositions as Types अवधारणा से जुड़ा है
    dependent types runtime पर कैसे काम करते हैं, और क्या compile व runtime दोनों पर type-checking चाहिए, यह जानने की जिज्ञासा है
    implementation में indirection बढ़ने से जटिलता तो नहीं आती, यह भी सवाल है
  • “Python में 10×5 matrix type व्यक्त करना चाहता हूँ” का मतलब आख़िरकार यह नहीं कि class बनाकर उसे सीधे define कर दिया जाए?

• Dr. Paulson का तर्क यह नहीं है कि dependent types बुरे हैं, बल्कि वे अनिवार्य नहीं हैं
  Lean की performance समस्याओं या intensional equality से जुड़ी चर्चा और होती तो अच्छा होता
  Isabelle के HEq(लिंक) की तरह, जब definitional equality नहीं होती तब समस्या पैदा होती है
  इसलिए मुझे लगता है कि dependent types का इस्तेमाल जितना संभव हो उतना कम करना बेहतर है
  ACL2 जैसे static typing के बिना सिस्टम में भी पर्याप्त verification संभव है
  आख़िरकार महत्वपूर्ण बात practicality और verifiability के बीच संतुलन है

  • software verification के दृष्टिकोण से Isabelle (non-dependent type) भी काफ़ी शक्तिशाली है
    Lean या Agda का उपयोग अभी industrial-scale verification में कम होता है
    Concrete Semantics(लिंक) और Logical Verification 2025(लिंक) की तुलना करना भी रोचक है
    व्यवहार में refinement types ज़्यादा व्यावहारिक हो सकते हैं
    उदाहरण: Rust Creusot, Dafny, LiquidHaskell का leftpad proof example
  • गणित में proofs को program की तरह नहीं लिखा जाता, इसलिए dependent types वहाँ अच्छी तरह काम करते हैं
    लेकिन program verification में “दो proofs समान हैं” जैसी जटिल auxiliary lemmas चाहिए होती हैं, और कई बार इन्हें सिद्ध करना संभव नहीं होता
  • “dependent types का इस्तेमाल जितना संभव हो उतना कम करना चाहिए” — इसका कारण जानना चाहूँगा
  • “ज़रूरी नहीं है” वाला तर्क कुछ हद तक बचने जैसा लगता है
    असली बात यह है कि कोई feature कितना उपयोगी है, न कि उसके अस्तित्व की अनिवार्यता
    आख़िरकार tool का चुनाव developer की पसंद और efficiency का मामला है

• यह दिलचस्प है कि आधुनिक logic की बहसों का बड़ा हिस्सा आख़िरकार सौंदर्यबोध की पसंद पर आ टिकता है
  अगर व्यावहारिक फ़ायदे बहुत निर्णायक होते, तो शायद बहस ही न होती
  संदर्भ के लिए Paulson और Lamport का 1999 का paper “Typing in Specification Languages” अच्छी पढ़ाई है
  बाद में Lamport के TLA+ जैसे informal formalism भी विकसित हुए

  • मैं इसे सिर्फ aesthetics का सवाल नहीं, बल्कि trade-off का सवाल मानता हूँ
    compile-time guarantee का लाभ मिलता है, लेकिन बदले में complexity और build time बढ़ते हैं
    असली सवाल यही है कि “क्या यह सौदा क़ीमती है?”

• HOL (simple type theory) की समस्या dependency नहीं, बल्कि logical strength की कमी है
  यह Zermelo set theory के सीमित संस्करण के बराबर है, इसलिए आधुनिक गणित को पूरी तरह formalize करने के लिए कमज़ोर पड़ता है
  खासकर category theory जैसे क्षेत्रों में size-related समस्याओं से निपटना कठिन होता है

  • Isabelle के locales feature का उपयोग करके Grothendieck schemes को formalize करने का एक उदाहरण है
    जिज्ञासा है कि यह असली गणितज्ञों की कार्यशैली से कितना अलग है
  • logical strength बढ़ाने के लिए axioms जोड़ना भी संभव है
    उदाहरण के लिए, ‘inaccessible cardinal’ जोड़ने से यह type theory के ‘universe’ concept जैसा हो जाता है

• मैं formal methods में विशेषज्ञता रखता था और dependent types मुझे बहुत आकर्षक लगते थे, लेकिन वास्तविक उपयोग हमेशा uphill battle जैसा रहा
  F# इस्तेमाल करते समय मैंने F* लाने की कोशिश की, लेकिन सहकर्मियों को उसकी mathematical learning curve भारी लगी
  अंत में मैं इस निंदक निष्कर्ष पर पहुँचा कि गणित वाले tools engineers आसानी से नहीं सीखते

  • F* गणित से ज़्यादा software verification-केंद्रित है, इसलिए उसका स्वभाव Lean से अलग है
    SMT-आधारित constraint solving की मदद से हल्के dependent-type usage संभव हो जाते हैं
    लेकिन “क्या यह सचमुच सही है” जैसे दार्शनिक सवालों का जवाब यह नहीं देता
    mathematical proof और software verification की दुनिया काफ़ी अलग है
  • लोग नई चीज़ें इसलिए नहीं नहीं सीखते कि वे सीखना नहीं चाहते, बल्कि इसलिए कि उन्हें investment के अनुपात में utility कम लगती है
    आख़िरकार समय सीमित है

• हमारी company Phosphor में हम dependent types को database/graph queries के साथ जोड़कर प्रयोग कर रहे हैं
  इससे RDF की सीमाओं को कुछ हद तक दूर किया गया और logic-based query system बनाया जा सका
  व्यवहार में हम TypeDB(typedb.com) का उपयोग कर रहे हैं, जो MongoDB से तेज़ है और जटिल data modeling में उपयोगी है
  यह Palantir की ontology अवधारणा से भी मिलता-जुलता है

  • “non-dilutive growth engine बनाया जा रहा है” — क्या इसे थोड़ा और ठोस रूप में समझाया जा सकता है?
  • TypeDB चुनने का कारण और वास्तविक performance metrics क्या हैं, यह जानना रोचक होगा

• आख़िरकार dependent types का रहस्य शायद यह जानना है कि इन्हें कब इस्तेमाल नहीं करना चाहिए
  Lean या Rocq की आलोचना करने के बजाय, शायद परिस्थिति के अनुसार Isabelle-शैली का दृष्टिकोण भी अपनाया जा सकता है

• Paulson टीम का Alexandria formalization project(लिंक) प्रभावशाली है
  खासकर quantum computing algorithm formalization research(paper link) बहुत दिलचस्प है

• पहले मुझे लगता था कि dependent types ही भविष्य हैं, लेकिन असली projects में productivity loss काफ़ी बड़ा था
  अब मैं ज़्यादा स्पष्ट और maintainable solutions को प्राथमिकता देता हूँ
  अगर कोई tool टीम के लिए समझने और बढ़ाने में आसान है, तो वही अच्छा tool है

• मुझे पूर्ण dependent types से ज़्यादा उनके किनारे पर मौजूद type systems पसंद हैं
  उदाहरण के लिए Purescript में Haskell की तुलना में ज़्यादा शक्तिशाली row-type built-in मिलता है,
  और type-level lists, strings, यहाँ तक कि regular expressions का भी समर्थन है
  इसे typeclass-आधारित logic programming शैली में भी इस्तेमाल किया जा सकता है