फ़ंक्शन रैप में EOF -> झूठी, ए -> ए ∀ ए ≠ ईओएफ का प्रतिनिधित्व करना?

Question

मैं Typed रैकेट में निम्नलिखित कार्य के लिए प्रकार एनोटेशन परिभाषित करने के लिए कोशिश कर रहा हूँ: एक त्रुटि का उत्पादन

(Any -> Any) 

इस प्रकार का उपयोग करना::

(define (neof x) 
    (if (eof-object? x) #f x)) 

यह अन-एनोटेट छोड़कर प्रकार देता है

(: neof (All (A) (case-> 
        (EOF -> False) 
        (A -> A : #:+ (! EOF)))) 

    expected: A 
    given: False 
    in: #f 

यह संभवतः है क्योंकि कोई A = EOF दे सकता है और फिर हमें EOF -> EOF मिल सकता है।

प्रकार (: neof (All (A) A -> (U A False) #:- (U EOF False))), जबकि के रूप में स्पष्ट नहीं ऊपर के रूप में, यह भी त्रुटियों देता है:

mismatch in filter 
    expected: (Top | Bot) 
    given: ((! (U False EOF) @ x) | ((U False EOF) @ x)) 
    in: (if (eof-object? x) #f x) 

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

(define/match (neof x) 
    [((? eof-object?)) #f] 
    [((? (compose not eof-object?))) x]) 

(इसके अलावा दूसरी पद्धति से किया जा रहा _, लेकिन उस प्रकार की जानकारी का एक ही राशि एन्कोड नहीं करता साथ इस बिंदु मैं पर:

पूर्णता के लिए, मैं भी neof की इस परिभाषा की कोशिश की किसी भी चीज़ से प्रकार चेकर को खुश करने की कोशिश कर रहा है)।

तो: मैं neof के प्रकार का प्रतिनिधित्व कैसे कर सकता हूं?

Answer 1

मुझे लगता है कि आप चाहते है:

(: neof (All (A) (A -> (U False A) : 
        #:+ (! EOF) 
        #:- (or EOF False)))) 

नोट (, मैं सिर्फ यह पूर्णता के लिए शामिल #:- खंड वैकल्पिक है।):#:- खंड हैं शामिल है, यह रैकेट 6.1.1 में टाइप चेक होगा। खंड को हटाने से इसे 6.1.1 पर जाने की अनुमति मिल जाएगी।

यहां मुद्दा यह है कि case-> की सभी शाखाओं को स्वतंत्र रूप से एक दूसरे के टाइपशेक करना होगा। (A -> A) मामले के लिए, यह विफल रहता है क्योंकि #fA नहीं है। पहले मामले से होने वाली घटना टाइपिंग जानकारी दूसरे मामले पर टाइपशेकिंग को प्रभावित नहीं कर सकती है।