लुआउमधील अर्थपूर्ण उपप्रकारीकरण

Luau ही पहिली प्रोग्रामिंग भाषा आहे जी सेमाँटिक सबटाइपिंगची शक्ती लाखो निर्मात्यांच्या हाती देते.

खोटे सकारात्मक निकाल कमी करणे

Roblox Studio मधील Script Analysis विजेटसारख्या साधनांमध्ये प्रकार त्रुटी अहवालाशी संबंधित समस्या म्हणजे खोट्या सकारात्मक अहवाल (false positives). हे विश्लेषणाचे उप-उत्पाद असून, रनटाइममध्ये उद्भवणाऱ्या त्रुटींशी त्यांचा संबंध नसतो. उदाहरणार्थ, प्रोग्राम

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 या दोन्ही प्रकारांनी गुणाकार (multiplication) समर्थित आहे. (त्याचा प्रकार ((CFrame, CFrame) -> CFrame) & ((CFrame, Vector3) -> Vector3) आहे.)

खोटे सकारात्मक परिणाम नव्या वापरकर्त्यांना सामील करण्यात विशेषतः अडथळा आणतात. जर एखादा प्रकाराबद्दल उत्सुक निर्माता टाइपचेकिंग चालू करतो आणि लगेचच खोटे लाल लहरींनी भरलेल्या भिंतीचा सामना करतो, तर त्याला ते त्वरित बंद करण्याची प्रबळ प्रेरणा मिळते.

प्रकार त्रुटींमधील अचूकतेचा अभाव अपरिहार्य आहे, कारण रनटाइम त्रुटी उद्भवणार की नाही हे आधी ठरवणे अशक्य आहे. प्रकार प्रणाली डिझाइनरना खोट्या सकारात्मक किंवा खोट्या नकारात्मक त्रुटींमधून एक निवडावी लागते. Luau मध्ये हे मोडद्वारे ठरते: strict मोड खोट्या सकारात्मक त्रुटींकडे झुकतो, तर nonstrict मोड खोट्या नकारात्मक त्रुटींकडे झुकतो.

अचूकतेतील त्रुटी अपरिहार्य असली तरी, त्या शक्य तितक्या वेळा दूर करण्याचा प्रयत्न करतो, कारण त्या चुकीच्या त्रुटी निर्माण करतात आणि autocomplete किंवा 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) चा उपप्रकार आहे का.

सबटाइपिंग हे एक अत्यंत उपयुक्त वैशिष्ट्य आहे, आणि हे type union (T | U) आणि intersection (T & U) सारख्या समृद्ध प्रकार रचनांना समर्थन देते. उदाहरणार्थ, number? हे union प्रकार (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?) चा एकमेव संभाव्य रहिवासी nil आहे.

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

या खोट्या सकारात्मक निष्कर्षांचा प्रकार आता Luau मध्ये उद्भवत नाही, कारण आम्ही वाक्यरचनात्मक उपप्रकार (syntactic subtyping) या आमच्या जुन्या पद्धतीपासून सेमॅंटिक उपप्रकार (semantic subtyping) नावाच्या पर्यायी पद्धतीकडे वळलो आहोत.

व्याकरणगत उपप्रकार

उर्फ "आम्ही पूर्वी जे केले."

संश्लेषणात्मक उपप्रकारीकरण हा एक वाक्यरचना-निर्देशित पुनरावर्ती अल्गोरिदम आहे. युनियन आणि इंटरसेक्शन प्रकारांशी संबंधित लक्षवेधी प्रकरणे अशी आहेत:

• प्रतिबिंबता: T हा T चा उपप्रकार आहे
• Intersection L: (T₁ & … & Tⱼ) ही U ची उपप्रकार आहे जेव्हा काही Tᵢ या U चे उपप्रकार असतात.
• Union 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 चे उपप्रकार नाही
• म्हणून Union L नुसार: (number?) हा nil चा उपप्रकार नाही.
• आणि: string हा nil चा उपप्रकार नाही
• म्हणून युनियन L नुसार: (string?) हा nil चा उपप्रकार नाही.
• म्हणून Intersection L नुसार: (number?) & (string?) हा nil चा उपप्रकार नाही.

हे वाक्यरचनात्मक उपप्रकारकरणाचे (syntactic subtyping) विशिष्ट वैशिष्ट्य आहे: जेव्हा ते "होय" परिणाम परत करते तेव्हा ते बरोबर असते, परंतु जेव्हा ते "नाही" परिणाम परत करते तेव्हा ते चुकीचे असू शकते. हा अल्गोरिदम एक संरक्षणात्मक अंदाज (conservative approximation) आहे, आणि "नाही" परिणामामुळे प्रकारातील त्रुटी (type errors) उद्भवू शकतात, ज्यामुळे खोटे सकारात्मक (false positives) निर्माण होतात.

अर्थगत उपप्रकार

ज्याला "आता आपण जे करतो" असेही म्हणतात.

सबटाइपिंगला सिंटॅक्स-निर्देशित मानण्याऐवजी, प्रथम त्याचे अर्थशास्त्र (semantics) पाहतो आणि नंतर त्याची अंमलबजावणी कशी केली जाते ते पाहतो. यासाठी, आम्ही अर्थशास्त्रीय सबटाइपिंग (semantic subtyping) अवलंबतो:

• प्रकाराचा अर्थ म्हणजे मूल्यांचा संच.
• Intersection प्रकार संचांच्या छेदनबिंदू म्हणून समजले जातात.
• युनियन प्रकार संचांच्या युनियन म्हणून समजले जातात.
• सबटाइपिंगला संच समावेश म्हणून पाहिले जाते.

उदाहरणार्थ:

आणि उपप्रकार संच समावेश म्हणून समजले जातात:

म्हणून सेमँटिक सबटाइपिंगनुसार, (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 किंवा फंक्शन प्रकारांच्या संमिलन इत्यादी)

एकदा प्रकार सामान्यीकृत झाल्यावर, अर्थपूर्ण उपप्रकार तपासणे सोपे होते.

प्रत्येक प्रकार सामान्यीकृत केला जाऊ शकतो (अहो, generic type packs बाबत काही तांत्रिक निर्बंध आहेत). महत्त्वाचे टप्पे आहेत:

• अनुरूप नसलेल्या प्रिमिटिव्ह्सच्या इंटरसेक्शन काढून टाकणे, उदा. number & bool या प्रकाराऐवजी never असा प्रकार बनवणे, आणि
• फंक्शन्सच्या युनियन काढून टाकणे, उदा. ((number?) -> number) | ((string?) -> string) याऐवजी (nil) -> (number | string).

उदाहरणार्थ, (number?) & (string?) चे सामान्यीकरण केल्यावर number & string काढून टाकले जाते, त्यामुळे फक्त nil उरते.

प्रकार सामान्यीकरण अंमलात आणण्याचा आमचा पहिला प्रयत्न मोकळेपणाने लागू केला गेला, परंतु यामुळे भयंकर कामगिरी झाली (जटिल कोड एका मिनिटापेक्षा कमी वेळात टाइपचेक होण्याऐवजी रात्रभर चालत असे). यामागचे कारण त्रासदायकपणे सोपे आहे: Luau च्या सबटाइपिंग अल्गोरिदममध्ये रिफ्लेक्सिव्हिटी (T हे T चे सबटाइप आहे) हाताळण्यासाठी एक ऑप्टिमायझेशन आहे, जे स्वस्त पॉइंटर समानता तपासणी करते. टाइप नॉर्मलायझेशन पॉइंटर-समान प्रकारांना अर्थदृष्ट्या समतुल्य (पण पॉइंटर-समान नसलेल्या) प्रकारांमध्ये रूपांतरित करू शकते, ज्यामुळे कामगिरी लक्षणीयरीत्या कमी होते.

या कामगिरीच्या समस्यांमुळे, आम्ही अजूनही सिंटॅक्टिक सबटाइपिंगला सबटाइपिंगसाठी पहिली तपासणी म्हणून वापरतो आणि फक्त सिंटॅक्टिक अल्गोरिदम अयशस्वी झाल्यासच प्रकार सामान्यीकरण (type normalization) करतो. हे तर्कसंगत आहे, कारण सिंटॅक्टिक सबटाइपिंग ही सेमाँटिक सबटाइपिंगची एक संरक्षणात्मक अंदाजपत्रक आहे.

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

तयार-उपलब्ध सेमँटिक सबटाइपिंग Luau मध्ये अंमलात आणलेल्या पद्धतीपेक्षा किंचित वेगळी आहे, कारण त्यासाठी मॉडेल सेट-थियरेटिक असणे आवश्यक असते, ज्यामुळे फंक्शन प्रकारांच्या घटकांनी "फंक्शनसारखे" वागावे लागते. आम्ही हा अट का काढून टाकतो याची दोन कारणे आहेत.

प्रथम, आम्ही फंक्शन प्रकारांचे सामान्यीकरण फंक्शन्सच्या इंटरसेक्शनमध्ये करतो, उदाहरणार्थ फंक्शन्सच्या युनियन्स आणि इंटरसेक्शन्सचा एक भयंकर गोंधळ:

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

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

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

सेट-थिओरेटिक सेमँटिक सबटाइपिंग हे सामान्यीकरण समर्थन करत नाही, आणि त्याऐवजी फंक्शन्सना विभक्त सामान्य स्वरूपात (फंक्शन्सच्या आंतरछेदांचे युनियन) सामान्यित करते. आम्ही हे वापरकर्ता अनुभवाच्या दृष्टीने टाळतो: Luau मध्ये ओव्हरलोड केलेले फंक्शन्स प्रचलित आहेत, परंतु DNF नाही, आणि आम्हाला वापरकर्त्यांना अशा अपारंपरिक प्रकारांसमोर आणायचे नाहीत.

आमचे सामान्यीकरण फंक्शन प्रकारांच्या युनियनचे पुनर्लेखन करून दूर करण्यावर अवलंबून आहे:

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

ही सामान्यीकरण आमच्या मॉडेलमध्ये वैध आहे, परंतु संच-सिद्धांत मॉडेलमध्ये नाही.

दुसरे म्हणजे, Luau मध्ये, फंक्शन ऍप्लिकेशनचा प्रकार f(x) हा B असतो जर f या प्रकाराचा प्रकार (A) -> B असेल आणि x या प्रकाराचा प्रकार A असेल. अप्रत्याशितपणे, रिक्त नसलेल्या प्रकारांमुळे हे संच-सिद्धांत मॉडेल्समध्ये नेहमीच खरे ठरत नाही. संच-सिद्धांत मॉडेल्समध्ये, जर x या प्रकाराचा प्रकार never असेल, तर f(x) या प्रकाराचा प्रकार never असतो. आम्हाला वापरकर्त्यांना फंक्शन अनुप्रयोगात एखादा विशेष कोपरा प्रकरण असतो, अशी कल्पना देऊन त्यांना त्रास द्यायचा नाही, विशेषतः कारण ते कोपरा प्रकरण फक्त मृत कोडमध्येच उद्भवू शकते.

सेट-थियॉरेटिक मॉडेल्समध्ये, (never) -> A हा (never) -> B चा उपप्रकार असतो, मग A आणि B काहीही असोत. हे Luau मध्ये खरे नाही.

या दोन कारणांसाठी (जे मुख्यतः तांत्रिक नसून वापरकर्ता अनुभवाशी संबंधित आहेत) आम्ही संच-सिद्धांतात्मक अट रद्द करून व्यावहारिक अर्थघटक उपप्रकारपद्धत (pragmatic semantic subtyping) वापरतो.

नकार प्रकार

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 सारख्या संरचनात्मक प्रकारांवर नाही, ज्यामुळे सामान्य नकारात्मक प्रकारांचा प्रसार टाळता येतो.

प्रोटोटाइपिंग आणि पडताळणी

Luau च्या सेमॅंटिक सबटाइपिंग अल्गोरिदमच्या डिझाइन दरम्यान बदल करण्यात आले (उदाहरणार्थ, सुरुवातीला आम्हाला वाटले की आम्ही सेट-थियॉरेटिक सबटाइपिंग वापरू शकू). या वेगवान बदलांच्या काळात, लवकर पुनरावृत्ती करणे महत्त्वाचे होते, म्हणून आम्ही थेट उत्पादन अंमलबजावणीकडे न जाता प्रथम एक प्रोटोटाइप अंमलात आणला.

प्रोटोटायपचे प्रमाणीकरण करणे महत्त्वाचे होते, कारण सबटाइपिंग अल्गोरिदममध्ये अनपेक्षित कोर्नर केसेस असू शकतात. या कारणास्तव, आम्ही प्रोटोटायपिंग भाषा म्हणून Agda स्वीकारली. युनिट टेस्टिंगला समर्थन देण्याबरोबरच Agda यंत्रचालित पडताळणीलाही समर्थन देते, त्यामुळे आम्हाला डिझाइनवर आत्मविश्वास आहे.

प्रोटोटाइपमध्ये संपूर्ण Luau अंमलात आणलेले नाही, फक्त कार्यात्मक उपसमूह आहे, परंतु उत्पादनमधील कदाचित दुरुस्त करणे कठीण असलेल्या बग्सच्या स्वरूपात समोर येणाऱ्या सूक्ष्म वैशिष्ट्य परस्परसंवादांचा शोध घेण्यासाठी हे पुरेसे होते.

प्रोटोटायपिंग परिपूर्ण नाही, उदाहरणार्थ, प्रॉडक्शनमध्ये आम्हाला जे मुख्य समस्या आढळल्या त्या कामगिरी आणि C++ स्टँडर्ड लायब्ररीबद्दल होत्या, ज्या प्रोटोटायपद्वारे कधीच पकडल्या जाणार नाहीत. पण प्रॉडक्शनची अंमलबजावणी इतरथा तुलनेने सोपी होती (किंवा किमान 3kLOC बदलाइतकी सोपी असू शकते).

पुढील पावले

सेमाँटिक सबटाइपिंगने खोटे सकारात्मक निष्कर्ष येण्याचे एक कारण दूर केले आहे, परंतु अजूनही काही शोधून काढावयाचे आहेत:

• ओव्हरलोड केलेल्या फंक्शनचे अनुप्रयोग आणि ऑपरेटर
• जटिल प्रकाराच्या अभिव्यक्तींवर गुणधर्म प्रवेश
• टेबलच्या फक्त-वाचनीय गुणधर्म
• काळाच्या ओघात प्रकार बदलणारे चल (ज्याला typestates म्हणतात)

मिथ्या लाल लहरी काढून टाकण्याचा शोध सुरूच आहे!

कृतज्ञता

या पोस्टच्या मसुद्यांवर उपयुक्त टिप्पण्या केल्याबद्दल ज्यूसेप्पे कास्टाग्ना आणि बेन ग्रीनमन यांचे आभार.

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