ओकैमल 'अंडरस्कोर प्रकार' (उदा। '_ ए) रनटाइम प्रकार त्रुटियों/ध्वनिता उल्लंघनों की संभावना का परिचय देते हैं?

Question

मैं मानक एमएल में मूल्य प्रतिबंध के बारे में थोड़ा सा पढ़ रहा था और यह देखने के लिए ओकैमल को उदाहरण का अनुवाद करने की कोशिश की कि यह क्या करेगा। ऐसा लगता है जैसे ओकैमल इन प्रकारों को संदर्भों में उत्पन्न करता है जहां एसएमएल मूल्य प्रतिबंध के कारण एक प्रोग्राम को अस्वीकार कर देगा। मैंने उन्हें अन्य संदर्भों में भी देखा है जैसे रिक्त हैश टेबल जो अभी तक किसी विशेष प्रकार के "विशेष" नहीं हैं।

http://mlton.org/ValueRestriction

यहाँ एसएमएल में एक को अस्वीकार कर दिया कार्यक्रम का एक उदाहरण है:

val r: 'a option ref = ref NONE 
val r1: string option ref = r 
val r2: int option ref = r 
val() = r1 := SOME "foo" 
val v: int = valOf (!r2) 

आप न्यू जर्सी के एसएमएल में शब्दशः पहली पंक्ति दर्ज करते हैं Repl आप प्राप्त निम्न त्रुटि:

- val r: 'a option ref = ref NONE; 
stdIn:1.6-1.33 Error: explicit type variable cannot be generalized at its binding declaration: 'a 

यदि आप स्पष्ट प्रकार की एनोटेशन छोड़ देते हैं तो आपको

मिलता है

- val r = ref NONE 

stdIn:1.6-1.18 Warning: type vars not generalized because of 
    value restriction are instantiated to dummy types (X1,X2,...) 
val r = ref NONE : ?.X1 option ref 

यह डमी प्रकार वास्तव में क्या है? ऐसा लगता है यह पूरी तरह से दुर्गम है जैसे और, कुछ भी

- r := SOME 5; 

stdIn:1.2-1.13 Error: operator and operand don't agree [overload conflict] 
    operator domain: ?.X1 option ref * ?.X1 option 
    operand:   ?.X1 option ref * [int ty] option 
    in expression: 
    r := SOME 5 

OCaml में साथ एकजुट करने के लिए इसके विपरीत द्वारा विफल रहता है, डमी प्रकार चर सुलभ है और पहली बात यह कर सकते हैं के साथ सम्मिलित है।

# let r : 'a option ref = ref None;; 
val r : '_a option ref = {contents = None} 

# r := Some 5;; 
- : unit =() 
# r ;; 
- : int option ref = {contents = Some 5} 

यह भ्रमित करने और कुछ प्रश्न उठाता है।

1) क्या एक अनुरूप एसएमएल कार्यान्वयन "डमी" प्रकार को सुलभ बनाने के लिए चुन सकता है?

2) ओकैमल मूल्य प्रतिबंध के बिना ध्वनि कैसे बनाए रखता है? क्या यह एसएमएल की तुलना में कमजोर गारंटी देता है?

3) '_a option ref'a option ref से कम polymorphic लगता है। OCaml में let r : 'a option ref = ref None;; (एक स्पष्ट एनोटेशन के साथ) क्यों खारिज नहीं किया गया है?

Answer 1

1) Could a conforming SML implementation choose to make the "dummy" type above accessible?

संशोधित परिभाषा (SML97) निर्दिष्ट नहीं करता एक "डमी" प्रकार हो कि; यह औपचारिक रूप से निर्दिष्ट करता है कि val एक पॉलिमॉर्फिक प्रकार चर लागू नहीं कर सकता है, क्योंकि दाएं हाथ की तरफ अभिव्यक्ति एक गैर-विस्तारक अभिव्यक्ति नहीं है। (शीर्ष चर में लीक नहीं होने वाले प्रकार चर के बारे में कुछ टिप्पणियां भी हैं, लेकिन जैसे ही एंड्रियास रॉसबर्ग अपने Defects in the Revised Definition of Standard ML में बताते हैं, ये टिप्पणियां वास्तव में परिभाषा के औपचारिकता में दिखाई देने वाले प्रकार चर के बजाय अनिश्चित प्रकार के बारे में हैं, इसलिए वे कर सकते हैं 'टी वास्तव में आवश्यकताओं के भाग के रूप में लिया जा)

अभ्यास में, मुझे लगता है कि चार दृष्टिकोण है कि कार्यान्वयन ले रहे हैं:।

• कुछ कार्यान्वयन के दौरान प्रकार-चेकिंग प्रभावित घोषणाओं अस्वीकार करते हैं, और प्रोग्रामर के लिए मजबूर एक monomorphic प्रकार निर्दिष्ट करने के लिए।
• कुछ कार्यान्वयन, जैसे कि एमएलटन, सामान्यीकरण को रोकें, लेकिन एकीकरण को स्थगित करें, ताकि उचित मोनोमोर्फिक प्रकार प्रोग्राम में बाद में स्पष्ट हो सके।
• जैसा कि आपने देखा है, एसएमएल/एनजे, एक चेतावनी जारी करता है और एक डमी प्रकार को तुरंत चालू करता है जिसे बाद में किसी अन्य प्रकार से एकीकृत नहीं किया जा सकता है।
• मुझे लगता है कि मैंने सुना है कि कुछ कार्यान्वयन int पर डिफ़ॉल्ट हैं? मुझे यकीन नहीं है।

इन विकल्पों में से सभी संभवतः अनुमति दी जाती है और जाहिरा तौर पर ध्वनि, हालांकि "एकीकरण स्थगित" दृष्टिकोण सुनिश्चित करने के लिए है कि प्रकार एक रूप में अभी तक ungenerated प्रकार का नाम (विशेष रूप से एक प्रकार नाम के साथ एकजुट नहीं है देखभाल की आवश्यकता होती है एक मज़ेदार के अंदर से, तब से मोनोमोर्फिक प्रकार मज़ेदार के विभिन्न अनुप्रयोगों में विभिन्न प्रकारों के अनुरूप हो सकता है, जो नियमित रूप से नियमित पॉलिमॉर्फिक प्रकार के रूप में समान प्रकार की समस्याएं होती हैं)।

2) How does OCaml preserve soundness without the value restriction? Does it make weaker guarantees than SML does?

मैं ओकैमल से बहुत परिचित नहीं हूं, लेकिन जो भी आप लिखते हैं, ऐसा लगता है जैसे यह एमएलटन के समान दृष्टिकोण का उपयोग करता है; इसलिए, इसे दृढ़ता बलिदान नहीं करना चाहिए।

(वैसे,, OCaml के बावजूद आप क्या संकेत करता है मूल्य प्रतिबंध है। वहाँ OCaml में मूल्य प्रतिबंध और एसएमएल में एक के बीच कुछ मतभेद हैं, लेकिन अपने कोड-के टुकड़े में से कोई भी उन मतभेदों से संबंधित है । है कि एक की तरह लगता है, हाँ, - अपने कोड के टुकड़े कितना प्रतिबंध OCaml बनाम एसएमएल में से एक कार्यान्वयन में लागू की जाती है में कुछ मतभेद

3) The type '_a option ref seems less polymorphic than 'a option ref . Why isn't let r : 'a option ref = ref None;; (with an explicit annotation) rejected in OCaml?

फिर प्रदर्शित), मैं OCaml साथ बहुत परिचित नहीं हूँ, लेकिन। मुझे गलती!

Answer 2

कमजोर पॉलिमॉर्फिक प्रकार ('_-स्टाइल प्रकार) टाइप सिस्टम के सही विस्तार के बजाय प्रोग्रामिंग सुविधा हैं।

2) How does OCaml preserve soundness without the value restriction? Does it make weaker guarantees than SML does?

OCaml मूल्य प्रतिबंध त्याग नहीं है, यह बजाय एक अनुमानी व्यवस्थित ref None की तरह है जिसका प्रकार मूल्यों के प्रकार व्याख्या से बचाता है कि लागू करता है केवल "साप्ताहिक" बहुरूपी है। वर्तमान "संकलन इकाई" को देखकर यह ह्युरिस्टिक: यदि यह साप्ताहिक पॉलिमॉर्फिक प्रकार के लिए वास्तविक प्रकार निर्धारित कर सकता है, तो सब कुछ काम करता है जैसे प्रारंभिक घोषणा उचित प्रकार की एनोटेशन थी, अन्यथा संकलन इकाई संदेश के साथ खारिज कर दी गई है:

# module A : sig val table : '_a option ref end = struct let option = ref None end;; 
Characters 27-30: 
    module A : sig val table : '_a option ref end = struct let option = ref None end;; 
          ^^^ 
Error: The type variable name '_a is not allowed in programs 

यह करना संभव है:

Error: The type of this expression, '_a option ref, 
     contains type variables that cannot be generalized 

3) The type '_a option ref seems less polymorphic than 'a option ref. Why isn't let r : 'a option ref = ref None;; (with an explicit annotation) rejected in OCaml?

इसका कारण यह है '_a एक "वास्तविक" प्रकार, नहीं है उदाहरण के लिए यह एक हस्ताक्षर स्पष्ट रूप से इस "प्रकार" का मान निर्धारित करने लिखने के लिए मना किया है है से बचने इन कमजोर polymorphic प्रकारों का उपयोग करके पुनरावर्ती रूप से polymorphic परिवर्तनीय घोषणा को पैक करने के लिए रिकर्सिव घोषणाओं का उपयोग करके और बाद के फ़ंक्शन उपयोग को टाइप परिभाषा को पूरा करता है, उदा।:

# let rec r = ref None and set x = r := Some(x + 1);; 
val r : int option ref = {contents = None} 
val set : int -> unit = <fun> 

Answer 3

अपने आखिरी सवाल के दूसरे भाग का जवाब करने के लिए,

3) [...] Why isn't let r : 'a option ref = ref None;; (with an explicit annotation) rejected in OCaml?

है ऐसा इसलिए है क्योंकि OCaml प्रकार एनोटेशन में होने वाली प्रकार चर की एक अलग व्याख्या है: यह के रूप में उन्हें व्याख्या existentially, मात्रा निर्धारित नहीं सार्वभौमिक रूप से प्रमाणित।यही है, कुछ इसके चर के संभावित तत्कालता के लिए केवल सभी के लिए एक प्रकार का एनोटेशन होना सही है। उदाहरण के लिए, यहां तक ​​कि

let n : 'a = 5 

ओकैमल में पूरी तरह से मान्य है। तर्कसंगत रूप से, यह बल्कि भ्रामक है और सर्वोत्तम डिजाइन विकल्प नहीं है।

OCaml में बहुरूपता को लागू करने के लिए, आप की तरह

let n : 'a. 'a = 5 

कुछ जो वास्तव में एक त्रुटि का कारण होता है लिखने के लिए की है। हालांकि, यह स्थानीय क्वांटिफायर प्रस्तुत करता है, इसलिए अभी भी एसएमएल से कुछ अलग है, और उदाहरणों के लिए काम नहीं करता है जहां 'a को कहीं और बाध्य करने की आवश्यकता है, उदा। निम्नलिखित:

fun pair (x : 'a) (y : 'a) = (x, y) 

OCaml में, आप

let pair : 'a. 'a -> 'a -> 'a * 'a = fun x y -> (x, y)