लुआउ में सेमांटिक सबटाइपिंग

Luau पहली प्रोग्रामिंग भाषा है जिसने लाखों रचनाकारों के हाथों में सेमांटिक सबटाइपिंग की शक्ति सौंपी है।

गलत सकारात्मक परिणामों को कम करना

Roblox Studio में Script Analysis विजेट जैसे टूल्स में टाइप एरर रिपोर्टिंग की एक समस्या झूठी सकारात्मक रिपोर्टें हैं। ये चेतावनियाँ विश्लेषण के परिणामस्वरूप उत्पन्न होती हैं, और रनटाइम पर होने वाली त्रुटियों से मेल नहीं खातीं। उदाहरण के लिए, प्रोग्राम

local x = CFrame.new()
local y
if math.random() < 0.5 then
  y = CFrame.new()
else
  y = Vector3.new()
end
local z = x * y

एक टाइप एरर की रिपोर्ट करता है जो रनटाइम पर नहीं हो सकती, क्योंकि CFrame, Vector3 और CFrame दोनों से गुणा का समर्थन करता है। (इसका टाइप ((CFrame, CFrame) -> CFrame) & ((CFrame, Vector3) -> Vector3) है।)

गलत सकारात्मक (False positives) नए उपयोगकर्ताओं को ऑनबोर्ड करने के लिए विशेष रूप से खराब होते हैं। यदि कोई प्रकार-जिज्ञासु (type-curious) निर्माता टाइपचेकिंग चालू करता है और तुरंत ही झूठी लाल लकीरों की दीवार का सामना करता है, तो उसे तुरंत इसे फिर से बंद करने का एक मजबूत प्रोत्साहन मिलता है।

टाइप त्रुटियों में अशुद्धियाँ अपरिहार्य हैं, क्योंकि यह पहले से तय करना असंभव है कि कोई रनटाइम त्रुटि ट्रिगर होगी या नहीं। टाइप सिस्टम डिजाइनरों को यह चुनना होता है कि वे फर्जी सकारात्मक (false positives) के साथ जिएँ या फर्जी नकारात्मक (false negatives) के साथ। लुआउ (Luau) में यह मोड द्वारा निर्धारित किया जाता है: strict मोड फर्जी सकारात्मकों की ओर त्रुटि करता है, और nonstrict मोड फर्जी नकारात्मकों की ओर त्रुटि करता है।

हालाँकि त्रुटियाँ अपरिहार्य हैं, हम जब भी संभव हो उन्हें दूर करने का प्रयास करते हैं, क्योंकि ये झूठी त्रुटियों और ऑटो-कम्प्लीट या API दस्तावेज़ीकरण जैसे टाइप-चालित उपकरणों में अस्पष्टता का कारण बनती हैं।

सबटाइपिंग झूठी सकारात्मकताओं का स्रोत

Luau (और TypeScript या Flow जैसी कई अन्य समान भाषाओं) में फाल्स पॉजिटिव्स के स्रोतों में से एक सबटाइपिंग है। सबटाइपिंग का उपयोग तब किया जाता है जब कोई वेरिएबल इनिशियलाइज़ किया जाता है या उसे असाइन किया जाता है, और जब कोई फ़ंक्शन कॉल किया जाता है: टाइप सिस्टम यह जांचता है कि एक्सप्रेशन का प्रकार वेरिएबल के प्रकार का सबटाइप है। उदाहरण के लिए, यदि हम उपरोक्त प्रोग्राम में टाइप जोड़ते हैं

local x : CFrame = CFrame.new()
local y : Vector3 | CFrame
if math.random() < 0.5 then
  y = CFrame.new()
else
  y = Vector3.new()
end
local z : Vector3 | CFrame = x * y

तो टाइप सिस्टम यह जांचता है कि CFrame गुणा का प्रकार (CFrame, Vector3 | CFrame) -> (Vector3 | CFrame) का उपप्रकार है।

सबटाइपिंग एक बहुत उपयोगी सुविधा है, और यह टाइप यूनियन (T | U) और इंटरसेक्शन (T & U) जैसे समृद्ध टाइप संरचनाओं का समर्थन करती है। उदाहरण के लिए, number? को एक यूनियन टाइप (number | nil) के रूप में लागू किया गया है, जिसमें वे मान होते हैं जो या तो संख्याएँ या nil होते हैं।

दुर्भाग्यवश, सबटाइपिंग का इंटरसेक्शन और यूनियन टाइप्स के साथ इंटरैक्शन अजीब परिणाम दे सकता है। पुराने Luau में एक सरल (लेकिन काफी कृत्रिम) उदाहरण था:

local x : (number?) & (string?) = nil
local y : nil = nil
y = x -- Type '(number?) & (string?)' could not be converted into 'nil'
x = y

यह त्रुटि सबटाइपिंग की विफलता के कारण होती है, पुराना सबटाइपिंग एल्गोरिदम रिपोर्ट करता है कि (number?) & (string?) nil का उपप्रकार नहीं है। यह एक फर्जी सकारात्मक परिणाम है, क्योंकि number & string में कोई मान नहीं है, इसलिए (number?) & (string?) का एकमात्र संभावित निवासी nil है।

यह एक कृत्रिम उदाहरण है, लेकिन इन समस्याओं के कारण रचनाकारों द्वारा वास्तविक मुद्दे उठाए गए हैं, उदाहरण के लिए https://devforum.roblox.com/t/luau-recap-july-2021/1382101/5। वर्तमान में, ये मुद्दे मुख्य रूप से उन निर्माताओं को प्रभावित करते हैं जो परिष्कृत टाइप सिस्टम सुविधाओं का उपयोग करते हैं, लेकिन जैसे-जैसे हम टाइप इंफरेंस को अधिक सटीक बनाते हैं, यूनियन और इंटरसेक्शन टाइप्स और भी आम हो जाएँगे, यहाँ तक कि बिना टाइप एनुएशन वाले कोड में भी।

गलत सकारात्मकों का यह वर्ग अब लुआउ में नहीं होता, क्योंकि हम सिंटैक्टिक सबटाइपिंग के अपने पुराने दृष्टिकोण से सेमंटिक सबटाइपिंग नामक एक वैकल्पिक दृष्टिकोण पर चले गए हैं।

संवादात्मक उपप्रकारकरण

अर्थात् "हम पहले जो करते थे।"

सिंटैक्टिक सबटाइपिंग एक सिंटैक्स-निर्देशित पुनरावर्ती एल्गोरिदम है। इंटरसेक्शन और यूनियन टाइप्स से निपटने के लिए दिलचस्प मामले हैं:

• प्रतिबिंबता: T T का एक उपप्रकार है
• Intersection L: (T₁ & … & Tⱼ) एक सबटाइप है U जब भी कुछ Tᵢ के सबटाइप होते हैं U
• संघ L: (T₁ | … | Tⱼ) एक उपप्रकार है U का जब सभी Tᵢ उपप्रकार हों U का
• Intersection R: T एक उपप्रकार है (U₁ & … & Uⱼ) का, जब भी T सभी Uᵢ का उपप्रकार हो।
• संघ R: T (U₁ | … | Uⱼ) का एक उपप्रकार है जब T कुछ Uᵢ का उपप्रकार है।

उदाहरण के लिए:

• रिफ्लेक्सिविटी द्वारा: nil एक उपप्रकार है nil का
• तो यूनियन R द्वारा: nil एक उपप्रकार है number? का
• और: nil एक उपप्रकार है string? का
• तो Intersection R द्वारा: nil (number?) & (string?) का एक उपप्रकार है।

याय! दुर्भाग्यवश, इन नियमों का उपयोग करके:

• number nil का उपप्रकार नहीं है
• तो यूनियन L के अनुसार: (number?) nil का उपप्रकार नहीं है
• और: string nil का उपप्रकार नहीं है
• तो यूनियन L द्वारा: (string?) nil का उपप्रकार नहीं है।
• तो Intersection L द्वारा: (number?) & (string?) nil का उपप्रकार नहीं है।

यह सिंटैक्टिक सबटाइपिंग की विशिष्टता है: जब यह "हाँ" परिणाम देता है, तो यह सही होता है, लेकिन जब यह "नहीं" परिणाम देता है, तो यह गलत हो सकता है। यह एल्गोरिदम एक रूढ़िवादी अनुमान है, और चूंकि "नहीं" परिणाम टाइप त्रुटियों का कारण बन सकता है, यह झूठी सकारात्मकताओं का स्रोत है।

सेमांटिक सबटाइपिंग

अर्थात् "अब हम जो करते हैं।"

सबटाइपिंग को सिंटैक्स-निर्देशित मानने के बजाय, हम पहले इसके अर्थशास्त्र (semantics) पर विचार करते हैं, और बाद में इस पर लौटते हैं कि इस अर्थशास्त्र को कैसे लागू किया जाता है। इसके लिए, हम अर्थगत सबटाइपिंग (semantic subtyping) को अपनाते हैं:

• किसी प्रकार का अर्थमूलकता मानों का एक समूह है।
• इंटरसेक्शन टाइप्स को सेट्स के इंटरसेक्शन के रूप में सोचा जाता है।
• यूनियन टाइप्स को सेट्स के यूनियन के रूप में सोचा जाता है।
• सबटाइपिंग को सेट समावेशन के रूप में माना जाता है।

उदाहरण के लिए:

और चूंकि उपप्रकारों को सेट समावेशन के रूप में व्याख्यायित किया जाता है:

तो सेमांटिक सबटाइपिंग के अनुसार, (number?) & (string?) nil के बराबर है, लेकिन सिंटैक्टिक सबटाइपिंग केवल एक दिशा का समर्थन करती है।

यह सब ठीक है, लेकिन अगर हम टूल्स में सेमांटिक सबटाइपिंग का उपयोग करना चाहते हैं, तो हमें एक एल्गोरिदम की आवश्यकता है, और पता चलता है कि सेमांटिक सबटाइपिंग की जाँच करना आसान नहीं है।

सेमांटिक सबटाइपिंग कठिन है

सटीक रूप से कहें तो यह NP-कठिन है।

हम ग्राफ़ रंगने की समस्या को सेमांटिक सबटाइपिंग में बदल सकते हैं, इसके लिए ग्राफ़ को एक Luau प्रकार के रूप में कोड किया जाता है, ताकि प्रकारों पर सबटाइपिंग की जाँच करने का परिणाम ग्राफ़ को रंगने की असंभवता की जाँच करने के समान हो।

उदाहरण के लिए, तीन-नोड, दो रंगों वाले ग्राफ़ को रंगना टाइप का उपयोग करके किया जा सकता है:

type Red = "red"
type Blue = "blue"
type Color = Red | Blue
type Coloring = (Color) -> (Color) -> (Color) -> boolean
type Uncolorable = (Color) -> (Color) -> (Color) -> false

फिर एक ग्राफ़ को एक ओवरलोड फ़ंक्शन टाइप के रूप में एन्कोड किया जा सकता है, जिसमें सबटाइप Uncolorable और सुपरटाइप Coloring हो, एक ओवरलोडेड फ़ंक्शन के रूप में जो किसी बाधा के उल्लंघन पर false लौटाता है। प्रत्येक ओवरलोड एक बाधा को एन्कोड करता है। उदाहरण के लिए, एक रेखा की बाधाएँ कहती हैं कि सटे हुए नोड्स का रंग एक जैसा नहीं हो सकता:

type Line = Coloring
  & ((Red) -> (Red) -> (Color) -> false)
  & ((Blue) -> (Blue) -> (Color) -> false)
  & ((Color) -> (Red) -> (Red) -> false)
  & ((Color) -> (Blue) -> (Blue) -> false)

एक त्रिभुज भी इसी तरह है, लेकिन इसके अंत बिंदुओं का भी रंग एक जैसा नहीं हो सकता:

type Triangle = Line
  & ((Red) -> (Color) -> (Red) -> false)
  & ((Blue) -> (Color) -> (Blue) -> false)

अब, Triangle, Uncolorable का एक सबटाइप है, लेकिन Line नहीं है, क्योंकि लाइन 2-रंगी हो सकती है। इसे किसी भी रंगों की किसी भी सीमित संख्या वाले किसी भी सीमित ग्राफ़ के लिए सामान्यीकृत किया जा सकता है, और इसलिए सबटाइप चेकिंग NP-कठिन है।

हम इसके साथ दो तरीकों से निपटते हैं:

• हम मेमोरी की खपत को कम करने के लिए टाइपों को कैश करते हैं, और
• यदि प्रकारों का कैश बहुत बड़ा हो जाता है तो "कोड बहुत जटिल" त्रुटि के साथ हार मान लें।

आशा है कि व्यवहार में ऐसा बहुत कम ही सामने आएगा। इस बात के ठोस सबूत हैं कि स्टैंडर्ड एमएल (Standard ML) जैसी टाइप सिस्टम्स के अनुभव से पता चलता है कि व्यवहार में इस तरह की समस्याएं उत्पन्न नहीं होती हैं, जो EXPTIME-कम्प्लीट है, लेकिन व्यवहार में आपको टाइप के रूप में ट्यूरिंग मशीन टेप को कोड करने के लिए विशेष प्रयास करना पड़ता है।

टाइप सामान्यीकरण

सेमांटिक सबटाइपिंग का निर्णय करने के लिए उपयोग किया जाने वाला एल्गोरिदम टाइप नॉर्मलाइज़ेशन है। सिंटैक्स द्वारा निर्देशित होने के बजाय, हम पहले टाइप को नॉर्मलाइज़्ड होने के लिए फिर से लिखते हैं, फिर नॉर्मलाइज़्ड टाइप पर सबटाइपिंग की जाँच करते हैं।

एक सामान्यीकृत प्रकार निम्नलिखित का एक संघ है:

• एक सामान्यीकृत शून्य प्रकार (या तो never या nil)
• एक सामान्यीकृत संख्या प्रकार (या तो never या number)
• एक सामान्यीकृत बूलियन प्रकार (या तो never या true या false या boolean)
• एक सामान्यीकृत फ़ंक्शन प्रकार (never या फ़ंक्शन प्रकारों का कोई इंटरसेक्शन) आदि

एक बार प्रकारों का सामान्यीकरण हो जाने पर, अर्थगत उपप्रकारता की जाँच करना सरल हो जाता है।

हर प्रकार को सामान्यीकृत किया जा सकता है (हफ़्, जेनेरिक टाइप पैक्स के आसपास कुछ तकनीकी प्रतिबंधों के साथ)। महत्वपूर्ण चरण हैं:

• अनुपयुक्त प्रिमिटिव्स के इंटरसेक्शन को हटाना, उदाहरण के लिए number & bool को never से प्रतिस्थापित किया जाता है, और
• फंक्शंस के यूनियंस को हटाना, उदाहरण के लिए ((number?) -> number) | ((string?) -> string) को (nil) -> (number | string) से प्रतिस्थापित किया जाता है।

उदाहरण के लिए, (number?) & (string?) को सामान्य करने पर number & string हटा दिया जाता है, इसलिए जो बचता है वह केवल nil है।

टाइप नॉर्मलाइज़ेशन को लागू करने के हमारे पहले प्रयास में इसे बड़े पैमाने पर लागू किया गया था, लेकिन इसके परिणामस्वरूप प्रदर्शन बहुत खराब हुआ (जटिल कोड, जो एक मिनट से भी कम समय में टाइपचेक हो जाता था, वह रात भर चलने लगा)। इसका कारण परेशान करने वाला सरल है: लुआउ के सबटाइपिंग एल्गोरिदम में रिफ्लेक्सिविटी (T, T का एक सबटाइप है) को संभालने के लिए एक ऑप्टिमाइज़ेशन है जो एक सस्ता पॉइंटर समानता जाँच करता है। टाइप नॉर्मलाइज़ेशन पॉइंटर-समान प्रकारों को अर्थपूर्ण-तौर पर समतुल्य (लेकिन पॉइंटर-समान नहीं) प्रकारों में परिवर्तित कर सकता है, जो प्रदर्शन को काफी खराब कर देता है।

इन प्रदर्शन समस्याओं के कारण, हम अभी भी सबटाइपिंग के लिए अपनी पहली जाँच के रूप में सिंटैक्टिक सबटाइपिंग का उपयोग करते हैं, और केवल तभी टाइप नॉर्मलाइज़ेशन करते हैं जब सिंटैक्टिक एल्गोरिदम विफल हो जाता है। यह उचित है, क्योंकि सिंटैक्टिक सबटाइपिंग सेमांटिक सबटाइपिंग का एक रूढ़िवादी अनुमान है।

व्यावहारिक अर्थगत उपप्रकारता

तैयार-से-उपलब्ध सेमांटिक सबटाइपिंग लुओ (Luau) में लागू की गई से थोड़ी अलग है, क्योंकि इसके लिए मॉडलों का सेट-थ्योरेटिक होना आवश्यक है, जो यह मांग करता है कि फ़ंक्शन प्रकारों के निवासी "फ़ंक्शन की तरह काम करें"। हम इस आवश्यकता को हटाने के दो कारण हैं।

सबसे पहले, हम फ़ंक्शन प्रकारों को फ़ंक्शनों के एक इंटरसेक्शन में सामान्यीकृत करते हैं, उदाहरण के लिए फ़ंक्शनों के यूनियंस और इंटरसेक्शंस का एक भयानक गड़बड़झाला:

((number?) -> number?) | (((number) -> number) & ((string?) -> string?))

एक ओवरलोडेड फ़ंक्शन में सामान्यीकृत होता है:

((number) -> number?) & ((nil) -> (number | string)?)

सेट-थ्योरेटिक सेमांटिक सबटाइपिंग इस सामान्यीकरण का समर्थन नहीं करती है, और इसके बजाय फ़ंक्शनों को विविक्त सामान्य रूप (फ़ंक्शनों के अन्तर्संयोजनों के संघ) में सामान्यीकृत करती है। हम ऐसा उपयोगितावादी कारणों से नहीं करते हैं: लुआउ में ओवरलोडेड फ़ंक्शन स्वाभाविक हैं, लेकिन डीएनएफ (DNF) नहीं है, और हम उपयोगकर्ताओं को ऐसे गैर-स्वाभाविक प्रकार प्रस्तुत नहीं करना चाहते हैं।

हमारा सामान्यीकरण फ़ंक्शन प्रकारों के यूनियनों को पुनर्लेखन करके हटाने पर निर्भर करता है:

((A) -> B) | ((C) -> D)   →   (A & C) -> (B | D)

यह सामान्यीकरण हमारे मॉडल में सार्थक है, लेकिन सेट-थ्योरेटिक मॉडल में नहीं।

दूसरा, लुआउ में, एक फ़ंक्शन अनुप्रयोग का प्रकार f(x) है यदि f का प्रकार (A) -> B है और x का प्रकार A है। अप्रत्याशित रूप से, यह सेट-थ्योरेटिक मॉडलों में हमेशा सच नहीं होता, क्योंकि इन आबादहीन प्रकारों के कारण। सेट-थ्योरेटिक मॉडलों में, यदि x का प्रकार never है, तो f(x) का प्रकार never है। हम उपयोगकर्ताओं पर इस विचार का बोझ नहीं डालना चाहते कि फ़ंक्शन अनुप्रयोग का एक विशेष कोर्नर केस होता है, खासकर जब वह कोर्नर केस केवल मृत कोड में ही उत्पन्न हो सकता है।

सेट-थ्योरेटिक मॉडलों में, (never) -> A (never) -> B का एक सबटाइप है, चाहे A और B कुछ भी हों। यह Luau में सत्य नहीं है।

इन दो कारणों से (जो मुख्यतः तकनीकी से अधिक एर्गोनॉमिक्स से संबंधित हैं) हम सेट-थ्योरेटिक आवश्यकता को हटा देते हैं, और व्यावहारिक सेमांटिक सबटाइपिंग का उपयोग करते हैं।

नकार प्रकार

Luau की टाइप सिस्टम और ऑफ-द-शेल्फ सेमांटिक सबटाइपिंग के बीच एक और अंतर यह है कि Luau सभी नकारात्मक प्रकारों का समर्थन नहीं करता है।

नकारात्मक प्रकारों की आवश्यकता का सामान्य मामला सशर्त अभिव्यक्तियों के टाइपचेकिंग में होता है:

-- initially x has type T
if type(x) == "string" then
  --  in this branch x has type T & string
else
  -- in this branch x has type T & ~string
end

यह एक नकारात्मक प्रकार ~string का उपयोग करता है, जिसमें ऐसी मान शामिल हैं जो स्ट्रिंग नहीं हैं।

Luau में, हम केवल string, function, Part आदि जैसे टेस्ट टाइप्स पर ही इस प्रकार की टाइपिंग रिफाइनेमेंट की अनुमति देते हैं, न कि (A) -> B जैसे स्ट्रक्चरल टाइप्स पर, जिससे सामान्य नकारात्‍मक टाइप्स का मामला टल जाता है।

प्रोटोटाइपिंग और सत्यापन

लुआउ के सेमांटिक सबटाइपिंग एल्गोरिथम के डिज़ाइन के दौरान, बदलाव किए गए (उदाहरण के लिए शुरुआत में हम सोचते थे कि हम सेट-थ्योरेटिक सबटाइपिंग का उपयोग कर पाएंगे)। इस तेज़ बदलाव के समय में, जल्दी से पुनरावृत्ति करना महत्वपूर्ण था, इसलिए हमने सीधे प्रोडक्शन इम्प्लीमेंटेशन पर जाने के बजाय शुरुआत में एक प्रोटोटाइप लागू किया।

प्रोटोटाइप का मान्यकरण महत्वपूर्ण था, क्योंकि सबटाइपिंग एल्गोरिदम में अप्रत्याशित कोर्नर केस हो सकते हैं। इस कारण से, हमने प्रोटोटाइपिंग भाषा के रूप में Agda को अपनाया। यूनिट टेस्टिंग का समर्थन करने के साथ-साथ, Agda मैकेनाइज्ड वेरिफिकेशन का भी समर्थन करता है, इसलिए हमें डिज़ाइन पर भरोसा है।

प्रोटोटाइप लुआउ (Luau) को पूरी तरह से लागू नहीं करता है, बल्कि केवल इसके कार्यात्मक उपसमूह को लागू करता है, लेकिन यह उन सूक्ष्म सुविधा अंतःक्रियाओं को खोजने के लिए पर्याप्त था जो शायद उत्पादन में ऐसे बग के रूप में सामने आतीं जिन्हें ठीक करना मुश्किल होता।

प्रोटोटाइपिंग पूरी तरह से सही नहीं है, उदाहरण के लिए, प्रोडक्शन में हमें जो मुख्य समस्याएँ आईं, वे प्रदर्शन और C++ स्टैंडर्ड लाइब्रेरी से संबंधित थीं, जिन्हें एक प्रोटोटाइप कभी पकड़ नहीं पाएगा। लेकिन प्रोडक्शन इम्प्लीमेंटेशन अन्यथा काफी सीधा-सादा था (या कम से कम 3kLOC बदलाव जितना सीधा-सादा हो सकता है)।

अगले कदम

सेमांटिक सबटाइपिंग ने फर्जी सकारात्मक परिणामों (false positives) के एक स्रोत को हटा दिया है, लेकिन हमें अभी भी अन्य स्रोतों का पता लगाना है:

• ओवरलोडेड फ़ंक्शन अनुप्रयोग और ऑपरेटर
• जटिल प्रकार के अभिव्यक्तियों पर प्रॉपर्टी एक्सेस
• टेबलों के केवल-पठनीय गुण
• समय के साथ प्रकार बदलने वाले चर (जिन्हें टाइपस्टेट्स भी कहा जाता है)

झूठी लाल लकीरों को हटाने का अभियान जारी है!

कृतज्ञता

इस पोस्ट के मसौदों पर सहायक टिप्पणियों के लिए गिउसेपे कास्टाग्ना और बेन ग्रीनमैन का धन्यवाद।

एलन लुआउ टाइप सिस्टम के डिज़ाइन और कार्यान्वयन का समन्वय करते हैं, जो रॉब्लॉक्स स्टूडियो में विकास की कई विशेषताओं को आगे बढ़ाने में मदद करता है। डॉ. जेफरी के पास प्रोग्रामिंग भाषाओं में अनुसंधान का 30 से अधिक वर्षों का अनुभव है, वे कई ओपन-सोर्स सॉफ्टवेयर परियोजनाओं के सक्रिय सदस्य रहे हैं, और उन्होंने इंग्लैंड की ऑक्सफ़ोर्ड विश्वविद्यालय से डीफिल की उपाधि प्राप्त की है।