द्विदिश टाइपचेकिंग पहेली

• Grace में bidirectional typechecking के implementation में list के पहले element के type को पूरी list के element type की तरह इस्तेमाल किया जा रहा था, जिसकी वजह से port: 8080 field हट गई और गलत evaluation result मिला
• समस्या वाला उदाहरण { domain: "google.com" } और { domain: "localhost", port: 8080 } की list पर iterate करते हुए default port 443 इस्तेमाल करने वाला code था, और अपेक्षित [ "google.com:443", "localhost:8080" ] के बजाय [ "google.com:443", "localhost:443" ] लौट रहा था
• पुरानी list inference प्रक्रिया पहले element से List { domain: Text } infer करती थी, फिर बाकी elements को उसी type के अनुसार check करती थी, और elaboration प्रक्रिया में ऊपर वाले type में न होने वाली port field हटा दी जाती थी
• बदले हुए implementation में पहले हर element का type infer किया जाता है, फिर सबसे specific supertype निकाला जाता है, और हर element को उस type के अनुसार दोबारा check करके missing Optional values को null या some से भरा जाता है
• fix के बाद वही list List { domain: Text, port: Optional Natural } के रूप में infer होती है, जिसमें पहले record का port null बनता है और दूसरे record का port: 8080 some 8080 के रूप में बचा रहता है, इसलिए expected result मिलता है

---

Grace का list type inference bug

• Grace Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism पर आधारित bidirectional typechecking system इस्तेमाल करता है, और इस approach की सीमाओं को पार करने के लिए बने implementation hacks जमा होते-होते एक अजीब bug तक पहुँच गए
• समस्या वाला program authorities list को iterate करते हुए हर record के domain और port को bind करता था, और port न होने पर 443 को default value की तरह इस्तेमाल करने वाले list comprehension के रूप में लिखा गया था

let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for { domain, port = 443 } of authorities

in  "${domain}:${show port}"

• expected result [ "google.com:443", "localhost:8080" ] था, लेकिन bug वाले version में [ "google.com:443", "localhost:443" ] मिला, यानी दूसरे record की port: 8080 field पूरी तरह ignore हो गई
• समस्या evaluator में नहीं बल्कि typechecker में थी, और list type inference तथा typechecking के दौरान होने वाली elaboration दोनों ने इसमें भूमिका निभाई

Bidirectional typechecking और पुरानी list inference पद्धति की सीमा

• authorities list के लिए Grace जिस type की उम्मीद कर रहा था, वह यह था

List { domain: Text, port: Optional Natural }

• इसका मतलब है कि हर record में required domain: Text field हो, और port: Optional Natural field हो भी सकती है और नहीं भी
• लेकिन पुराना implementation वास्तव में इससे संकरा type infer करता था

>>> :type [ { "domain": "google.com" }, { "domain": "localhost", "port": 8080 } ]
List { domain: Text }

• Bidirectional typechecking आम तौर पर दो कामों में बँटा होता है
  • expression का type infer करना
  • expression expected type से मेल खाता है या नहीं, यह check करना
• सिर्फ इन दो operations से list के कई elements के types को जोड़कर पूरी list के element type का supertype आसानी से बनाना संभव नहीं होता
• पुराना Grace implementation list type को इस तरह infer करता था
  • list के पहले element का type infer करो
  • बाकी सभी elements को पहले element से infer हुए type के against check करो
• क्योंकि पहले element { domain: "google.com" } का type { domain: Text } था, इसलिए पूरी list का element type भी { domain: Text } बन गया
• अगर कोई दूसरा type चाहिए होता, तो explicit type annotation देनी पड़ती, लेकिन Grace जिन real-world JSON values को handle करना चाहता है, उनमें schema बड़ा और जटिल हो सकता है, इसलिए पूरी schema को एक विशाल type annotation के रूप में लिखवाना ठीक नहीं था

Elaboration ने evaluation result क्यों बदल दिया

• Grace का typechecker सिर्फ type errors पकड़ता ही नहीं, बल्कि typechecking के दौरान expressions को adjust करने वाली elaboration भी करता है
• जब किसी subtype को supertype के against check किया जाता है और दोनों types अलग होते हैं, तो typechecker explicit coercion insert करता है
• Grace evaluator अंदरूनी तौर पर सभी Optional values को null या some x tag वाले value के रूप में represent करता है
• अगर किसी जगह Optional expected हो और वहाँ बिना tag वाला value दिया गया हो, तो Grace अपने-आप some tag insert कर देता है

>>> [ some 1, 2 ]  # This would be a type mismatch without elaboration
[ some 1, some 2 ]

• अगर पहले element का type Optional Natural infer हो और दूसरा element बिना tag वाला Natural हो, तो typechecker type mismatch error देने के बजाय some tag insert करता है
• records में भी यही होता है, और Grace record subtyping को support करता है तथा record को expected supertype के हिसाब से coerce करता है

>>> { x: 1, y: true }: { x: Natural }
{ "x": 1 }

• जब किसी record पर छोटा record type annotation लगाया जाता है, तो typechecker इसे allow करता है और expected type में न होने वाली fields को हटा देता है
• सिर्फ authorities list को evaluate करने पर भी पुराने implementation में port field इस तरह हट जाती थी

>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com" }, { "domain": "localhost" } ]

• यह result इस flow से आता था
  • पहले element का type { domain: Text } infer होता है
  • दूसरे element को उसी expected type के against check किया जाता है
  • दूसरा element उस type से मेल खाता है, लेकिन उसमें extra port field है
  • expected type से match कराने के लिए typechecker port field हटा देता है
• record coercion खुद मूल कारण नहीं था; असली समस्या list type inference में पहले element के type को पूरी list के type की तरह मान लेने की पद्धति थी

समाधान: सबसे specific supertype की गणना

• Grace ने पूरी list का type सही infer करने के लिए नया operation जोड़ा
• यह नया operation दो types का most-specific supertype, यानी least upper bound निकालता है
• अगर C, A और B का supertype है, तो उसका मतलब है कि C, A का भी supertype है और B का भी
• अगर C, A और B का सबसे specific supertype है, तो इसका मतलब है कि C, A और B के हर दूसरे supertype का subtype भी है
• इस नए operation के साथ list type inference की प्रक्रिया इस क्रम में बदल गई
  • list के हर element का type infer करो
  • सभी element types का सबसे specific supertype निकालो
  • हर element को उस सबसे specific supertype के against check करो
  • उसी सबसे specific supertype को पूरी list के element type के रूप में return करो
• इस तरीके से नीचे दी गई list का type अब सही infer होता है

>>> :type [ { x: 1 }, { y: true } ]
List { x: Optional Natural, y: Optional Bool }

• अंदरूनी flow इस तरह है
  • { x: 1 } का type { x: Natural } infer होता है
  • { y: true } का type { y: Bool } infer होता है
  • दोनों types का सबसे specific supertype { x: Optional Natural, y: Optional Bool } बनता है
  • फिर हर element को उसी supertype के against check किया जाता है
• हर element को supertype के against दोबारा check करने की वजह यह है कि सही elaboration लागू हो सके, जैसे missing some और null भरना

>>> [ { x: 1 }, { y: true } ]
[ { "x": some 1, "y": null }, { "y": some true, "x": null } ]

fix के बाद authorities का type और evaluation result

• typechecker fix होने के बाद मूल authorities list वही expected type infer करती है

>>> :type [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
List { domain: Text, port: Optional Natural }

• elaborated evaluation result भी port को optional field के रूप में बचाए रखता है

>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com", "port": null }
, { "domain": "localhost", "port": some 8080 }
]

• पहले record का missing port null से भरा जाता है, और दूसरे record का port: 8080 some 8080 के रूप में बना रहता है
• मूल list comprehension उदाहरण भी अब expected result लौटाता है

[ "google.com:443", "localhost:8080" ]

JSON support और implementation complexity के बीच चुनाव

• Grace bidirectional typechecking पर इतना ज़ोर इसलिए देता है क्योंकि उसका मानना है कि यह approach, भले जटिल हो, लेकिन real-world JSON types को infer करने लायक मजबूत typechecking framework है
• Hindley-Milner inference या उससे मिलते-जुलते सरल typechecking frameworks, असली JSON data में दिखने वाले patterns को संभालने में कठिनाई महसूस करते हैं
• Grace सिर्फ JSON work के लिए बनी ergonomic language नहीं है, लेकिन उसने JSON support को नज़रअंदाज़ भी नहीं किया
• Dhall के अनुभव से यह सीखा गया कि users ergonomic JSON interoperability को लेकर बहुत संवेदनशील होते हैं, इसलिए Grace की syntax और type system को implementation complexity बढ़ने की कीमत पर भी JSON compatibility ध्यान में रखकर design किया गया

आगे पढ़ने लायक संबंधित सामग्री

• Datatype unification using Monoids: इसमें simple data type inference algorithm पर चर्चा है, जो Grace में सबसे specific supertype निकालने के लिए इस्तेमाल किए गए algorithm के मूल रूप से समान है
• The appeal of bidirectional typechecking: इसमें बताया गया है कि अगर आप किसी ऐसी language को implement करना चाहते हैं जो किसी न किसी रूप में subtyping इस्तेमाल करती हो, तो bidirectional typechecking सीखना क्यों उपयोगी है
• Local Type Inference: यह bidirectional typechecking पर शुरुआती papers में से एक है, और least upper bound तथा expressions को internal language में elaborate करने जैसी techniques का स्रोत बताया गया है

परिशिष्ट: record coercion की ज़रूरत क्यों है

• नीचे दिया गया Grace expression यह दिखाता है कि record coercion की ज़रूरत क्यों पड़ती है

let f (input: { }) = input.x

in  f { x: 1 }

• अगर यह expression typecheck होता है, तो सवाल उठता है कि f का return type क्या होना चाहिए
• return type Natural नहीं हो सकता

let f (record: { }): Natural = record.x  # WRONG: type error

in  f { x: 1 }

• f को { } type का input मिलता है, इसलिए वह उस record से Natural value नहीं निकाल सकता
• भले call site पर संयोग से x field वाला record pass किया गया हो, f को { } type के किसी भी input पर काम करना चाहिए
• typechecker अगर declared input type में न होने वाली field access को reject कर दे तो यह भी sound choice है, लेकिन फिर real JSON data को handle करने के लिए ज़रूरी functionality खो जाती है
• मूल authorities उदाहरण, मूल रूप से नीचे दिए गए expression की syntax sugar जैसा ही है

let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for authority of authorities

let default = fold{ some port: port, null: 443 }

in  "${authority.domain}:${show (default authority.port)}"

• अगर missing field access को reject कर दिया जाए, तो संभावित रूप से absent fields को bind करना या default value के साथ handle करना संभव नहीं रहेगा
• real JSON data को ठीक से handle करने के लिए design choice यह है
  • field न हो तो null return करो
  • access type को forall (a: Type) . Optional a मानो
• यह ऐसा type है जिसमें सिर्फ null ही हो सकता है
• इस approach को अपनाने पर record से उन fields को ज़रूर हटाना पड़ता है जो supertype में मौजूद नहीं हैं
• अगर extra fields न हटाई जाएँ, तो नीचे का उदाहरण 1 : forall (a: Type) . Optional a return करेगा

let f (input: { }) = input.x

in  f { x: 1 }

• यह गलत typed expression होगा, क्योंकि जिस type में सिर्फ null होना चाहिए उसमें 1 आ जाएगा
• ऐसा गलत expression evaluator को भी तोड़ सकता है

let f (input: { }) = input.x  # Inferred type: forall (a: Type). Optional a

let default (input: Optional Text) = fold{ some text: text, "" }

in  "${default (f { x: 1 })}!"  # Runtime error if `f` returns `1`

• real JSON data के साथ काम करने वाले Grace में record को supertype के अनुसार explicit रूप से coerce करना उचित व्यवहार है, और असली bug coercion में नहीं बल्कि List type inference के लिए इस्तेमाल किए जा रहे पुराने अस्थायी workaround में था

[GN⁺]

Lobste.rs की राय

• Complete And Easy पेपर को वास्तव में चलने वाली चीज़ के रूप में बनाना बधाई की बात है। यह इस बात का भी अच्छा उदाहरण है कि bidirectional type checking की greedy प्रकृति कैसे सूक्ष्म समस्याएँ पैदा कर सकती है
  यह आलोचना नहीं है; type inference में हमेशा समस्याएँ होती हैं, और आखिरकार बात इस पर आकर टिकती है कि आप किस तरह की समस्या स्वीकार करना चाहते हैं। इसलिए निजी तौर पर मुझे subtyping और type coercion ज़्यादातर anti-pattern के करीब लगते हैं
  अगर आप data को type के लिए truth source बना देते हैं, तो यह जाँचना कठिन हो जाता है कि data गलत है या नहीं, और उदाहरण की तरह उपयोगी error की जगह गलत type मिल जाता है। हालांकि Dhall बनाने वाले व्यक्ति इस विषय को मुझसे कहीं बेहतर जानते होंगे। कई data लेकर schema जनरेट करने का विचार अपने आप में शोध योग्य है, लेकिन type को आम तौर पर वर्णनात्मक के बजाय नियामक माना जाता है, इसलिए इसे “type checking” कहना सही होगा या नहीं, इस पर मुझे यक़ीन नहीं है

• यह बात मेरी समझ से बाहर है कि f को सीधे reject क्यों नहीं किया जाता। यह ऐसे record के field को access कर रहा है, जिसके type में वह field कभी हो ही नहीं सकता, इसलिए लगभग निश्चित रूप से यह program bug है और type checker को इसकी सूचना देनी चाहिए
  authority वाले उदाहरण से फर्क यह है कि port का type गायब नहीं है, बल्कि वह Optional है। missing field को reject करने का मतलब यह नहीं कि optional field को भी reject करना पड़े। अगर आप पहले से ही type के आधार पर values को coerce कर रहे हैं, तो { domain: "google.com" } को { domain: "google.com", port: null } में भी coerce किया जा सकता है

  • संक्षेप में, f को ज़रूरी नहीं कि reject ही किया जाए; वह अनावश्यक प्रतिबंध है। मुझे लगता है कि गलत field access के लिए null : forall (a : Type) . Optional a लौटाना, गलत field access को reject करने की तुलना में सख्ती से बेहतर है
    इससे अधिक valid programs स्वीकार किए जा सकते हैं, और गलत तरीके से typed programs फिर भी fail होंगे। उदाहरण के लिए, ऐसा program जो accessed value को null संभाले बिना इस्तेमाल करना चाहता है, उसमें type error वैसे ही बना रहेगा

• मेरी पहली प्रतिक्रिया यह है कि row types इस समस्या को हल कर देते हैं। लगता है यह पहले से विचार में रहा होगा। क्या यहाँ row types, subtyping के साथ interact करते हुए टूट जाते हैं?

  • Grace में row types और row polymorphism हैं। Grace में rows को “fields” कहा जाता है, लेकिन इसके अलावा बात पूरी तरह वही है
    वास्तव में, most specific supertype algorithm भी row types को ध्यान में रखता है
    उदाहरण के लिए, अगर आप इस तरह लिखें:

    \\record0 record1 ->
    
    let _ = record0.x
    
    let _ = record1.y
    
    in  [ record0, record1 ]  
    

    तो Grace इस expression के लिए यह type infer करता है:

    forall (a : Type) .  
    forall (b : Type) .  
    forall (c : Fields) .  
      { x: b, y: a, c } -> { y: a, x: b, c } -> List { x: b, y: a, c }  
    

• क्या यह Bidirectional Typing पेपर की धारा 5.1.1 में बताए गए greedy instantiation समस्या का उदाहरण नहीं है?
  “मूल सेटिंग में यह कुछ दुर्भाग्यपूर्ण था कि यह greedy तरीका argument order के प्रति संवेदनशील था। लेकिन predicate high-rank polymorphism की उस सेटिंग में, जहाँ subtyping के अन्य रूप नहीं हैं, यह अच्छी तरह काम कर सकता है। ‘tabby-first problem’ हो ही नहीं सकती, क्योंकि type के सख्ती से छोटा होने का एकमात्र तरीका सख्ती से अधिक polymorphic होना है, और अगर पहला argument polymorphic है, तो 𝛼 को polymorphic type से instantiate करना पड़ेगा, जो predicativity का उल्लंघन करेगा”