निर्भर टाइपिंग क्या है?

Question

क्या कोई मुझे निर्भर टाइपिंग समझा सकता है? मुझे हास्केल, केयेने, एपिग्राम, या अन्य कार्यात्मक भाषाओं में थोड़ा सा अनुभव है, इसलिए आप जिन शब्दों का उपयोग कर सकते हैं, उतना सरल, जितना अधिक मैं इसकी सराहना करता हूं!

Answer 1

इस पर विचार करें: सभी सभ्य प्रोग्रामिंग भाषाओं में आप कार्य लिख सकते हैं, उदा।

def f(arg) = result 

यहाँ, f एक मूल्य arg लेता है और एक मूल्य result गणना करता है। यह मूल्यों से मूल्यों का एक कार्य है।

अब, कुछ भाषाओं आप बहुरूपी (उर्फ सामान्य) मान निर्धारित करने की अनुमति:

def empty<T> = new List<T>() 

यहाँ, empty एक प्रकार T लेता है और एक मूल्य की गणना करता है। यह प्रकारों से मूल्यों का एक कार्य है।

आमतौर पर, आप भी सामान्य प्रकार परिभाषाएं हो सकता है:

type Matrix<T> = List<List<T>> 

इस परिभाषा एक प्रकार लेता है और यह एक प्रकार देता है। इसे प्रकार से प्रकारों के फ़ंक्शन के रूप में देखा जा सकता है।

सामान्य भाषाओं की पेशकश के लिए बहुत कुछ। एक भाषा को निर्भर रूप से टाइप किया जाता है यदि यह चौथी संभावना भी प्रदान करता है, अर्थात् मूल्यों से मूल्यों को परिभाषित करना। या दूसरे शब्दों में, एक मूल्य के ऊपर एक प्रकार परिभाषा parameterizing:

type BoundedInt(n) = {i:Int | i<=n} 

कुछ मुख्यधारा भाषाओं इस में से कुछ नकली रूप है कि भ्रमित होने की नहीं है। जैसे सी ++ में, टेम्पलेट पैरामीटर के रूप में मूल्य ले सकते हैं, लेकिन लागू होने पर उन्हें संकलन-समय स्थिरांक होना चाहिए। वास्तव में एक निर्भर रूप से टाइप की गई भाषा में नहीं। उदाहरण के लिए, मैं इस तरह से ऊपर प्रकार इस्तेमाल कर सकते हैं:

def min(i : Int, j : Int) : BoundedInt(j) = 
    if i < j then i else j 

संपादित करें: यहाँ, समारोह के परिणाम प्रकार वास्तविक तर्क मूल्य j, इस प्रकार शब्दावली पर निर्भर करता है।

Answer 2

पुस्तक प्रकार का हवाला देते हुए और प्रोग्रामिंग भाषाएं (30.5):

इस पुस्तक की ज्यादातर अमूर्त औपचारिकता विभिन्न प्रकार के तंत्र के साथ संबंध किया गया है। बस टाइप किए गए लैम्ब्डा-कैलकुस में, हम ने एक शब्द लेने और उपमहाद्वीप को निष्पादित करने के संचालन को औपचारिक रूप से कार्यान्वित किया, जिसमें एक ऐसा कार्य प्रस्तुत किया गया जिसे बाद में द्वारा इसे विभिन्न शर्तों पर लागू किया जा सके। सिस्टम F में, हमने एक शब्द लेने और एक प्रकार का सारण करने के संचालन को माना, शब्द प्रदान किया जिसे इसे विभिन्न प्रकारों में लागू करके तत्काल किया जा सकता है। λω में, हम बस टाइप किया लैम्ब्डा-पथरी के तंत्र recapitulated "एक स्तर ऊपर," एक प्रकार ले रहे हैं और एक प्रकार ऑपरेटर है कि बाद विभिन्न प्रकार पर लागू करके instantiated जा सकती है, प्राप्त करने के लिए एक उपसूचक बाहर सार संक्षेप। अमूर्तता के इन सभी रूपों के बारे में सोचने का एक सुविधाजनक तरीका अभिव्यक्ति के परिवारों के संदर्भ में है, जो अन्य अभिव्यक्तियों द्वारा अनुक्रमित है। एक साधारण लैम्ब्डा अमूर्तता λx:T1.t2 शर्तों [x -> s]t1s द्वारा अनुक्रमित [x -> s]t1 का एक परिवार है। इसी तरह, एक प्रकार का अबास्ट्रक्शन λX::K1.t2 प्रकारों द्वारा अनुक्रमित शब्दों का एक परिवार है, और एक प्रकार ऑपरेटर प्रकारों द्वारा अनुक्रमित प्रकारों का एक परिवार है।

• λx:T1.t2 शर्तों के परिवार शर्तों

• λX::K1.t2 शर्तों के परिवार प्रकार

• प्रकार

इस सूची को देखते हुए द्वारा अनुक्रमित प्रकार के परिवार λX::K1.T2 द्वारा अनुक्रमित द्वारा अनुक्रमित, यह स्पष्ट है कि एक संभावना है कि हम हे अभी तक नहीं माना गया है: शर्तों के अनुसार अनुक्रमित प्रकार के परिवार। इस अमूर्तता के रूप का भी व्यापक रूप से अध्ययन किया गया है, निर्भर प्रकार के रूब्रिक के तहत।

Answer 3

आप सी ++ पता करने के लिए यह एक प्रेरित उदाहरण प्रदान करने के लिए आसान है हो तो:

मान लीजिए कि हम कुछ कंटेनर के प्रकार और उसके

typedef std::map<int,int> IIMap; 
IIMap foo; 
IIMap bar; 

दो उदाहरणों है और इस कोड टुकड़ा पर विचार करें (आप कर सकते हैं मान foo गैर खाली है):

IIMap::iterator i = foo.begin(); 
bar.erase(i); 

यह स्पष्ट कचरा है (और शायद डेटा संरचना भ्रष्ट एस), लेकिन यह ठीक से टाइप-चेक करेगा क्योंकि "इटेटर इन फू" और "बार में इटरेटर" एक ही प्रकार हैं, IIMap::iterator, भले ही वे पूरी तरह से असंगत रूप से असंगत हैं।

foo.iterator i = foo.begin(); 
bar.erase(i); // ERROR: bar.iterator argument expected 

:

मुद्दा यह है कि पुनरावर्तक प्रकार कंटेनर पर कंटेनर प्रकार पर लेकिन वास्तव में सिर्फ निर्भर नहीं रहना चाहिए वस्तु, यानी यह एक "गैर स्थिर सदस्य प्रकार" होना चाहिए है

ऐसी सुविधा, एक प्रकार (foo.iterator) को व्यक्त करने की क्षमता जो एक शब्द (foo) पर निर्भर करती है, वास्तव में निर्भर टाइपिंग का अर्थ है।

कारण यह अक्सर आप इस सुविधा को नहीं देखते हैं क्योंकि यह कीड़े का एक बड़ा हिस्सा खुलता है: आप अचानक परिस्थितियों में समाप्त होते हैं, जहां संकलन-समय पर जांच करने के लिए, दो प्रकार समान होते हैं, आप समाप्त होते हैं दो अभिव्यक्तियों को साबित करने के लिए बराबर हैं (हमेशा रनटाइम पर समान मूल्य उत्पन्न करेंगे)। नतीजतन, यदि आप विकिपीडिया के list of dependently typed languages की तुलना अपने list of theorem provers के साथ करते हैं तो आपको एक संदिग्ध समानता दिखाई दे सकती है। ;-)

Answer 4

आश्रित प्रकार के बड़े सेट को संकलित समय पर समाप्त करने के लिए सक्षम करते हैं। इस समारोह f पर निम्नलिखित विनिर्देश पर विचार उदाहरण देकर स्पष्ट करने:

समारोह f इनपुट के रूप में केवल भी पूर्णांकों रखना चाहिए।

निर्भर प्रकार आप कुछ इस तरह कर सकते हैं बिना:

def f(n: Integer) := { 
    if n mod 2 != 0 then 
    throw RuntimeException 
    else 
    // do something with n 
} 

यहाँ संकलक अगर n पहचान नहीं कर सकता, वह है, संकलक के नजरिए से निम्नलिखित अभिव्यक्ति ठीक है यहां तक ​​कि वास्तव में है:

f(1) // compiles OK despite being a logic error! 

यह प्रोग्राम चलाएगा और फिर रनटाइम पर अपवाद फेंक देगा, यानी, आपके प्रोग्राम में तर्क त्रुटि है।

अब, निर्भर प्रकार आप और अधिक अर्थपूर्ण होने के लिए सक्षम और कुछ इस तरह लिखने के लिए सक्षम होगा:

def f(n: {n: Integer | n mod 2 == 0}) := { 
    // do something with n 
} 

यहाँ n निर्भर प्रकार {n: Integer | n mod 2 == 0} की है। यह संकलक संकलन समय पर पता लगाने के हैं इस मामले में द्वारा 2.

इस बाहर पढ़ने के लिए ऐसी है कि प्रत्येक पूर्णांक विभाज्य है जोर

रूप

n पूर्णांकों का एक सेट का एक सदस्य है मदद कर सकता है एक तर्क त्रुटि जहां f को एक विषम संख्या बीत चुके हैं और कार्यक्रम रोका जा सके पहली जगह में निष्पादित किया जाना है:

f(1) // compiler error