Darstellen der Funktion EOF -> Falsch, A -> A ∀ A ≠ EOF in getipptem Racket?

Question

Ich versuche, die Typanmerkung für die folgende Funktion in typisierten Racket zu definieren:

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

Verlassen sie un-kommentierten gibt den Typ:

(Any -> Any) 

Mit dieser Art erzeugt einen Fehler:

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

    expected: A 
    given: False 
    in: #f 

Dies ist vermutlich, weil man A = EOF lassen kann und dann erhalten wir EOF -> EOF.

Der Typ (: neof (All (A) A -> (U A False) #:- (U EOF False))), die zwar nicht so klar wie die oben, auch Fehler gibt:

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

Mein Ziel eine bekommen entweder False oder eine Funktion, die ich anwenden könnte auf jeden Ausgang von einem Hafen haben war Wert vom Port. Ich überdenke jetzt die Notwendigkeit dafür, da ich viel zu viel Zeit damit verbracht habe, diesen Typ herauszufinden.

Der Vollständigkeit halber habe ich auch versucht, diese Definition von neof.

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

(Auch mit dem zweiten Muster _ zu sein, aber das kodiert nicht für die gleiche Menge an Typ-Informationen An diesem Punkt bin ich mehr versuchen, den Typ Checker als alles zu beschwichtigen).

Also: wie kann ich den Typ neof darstellen?

Answer 1

Ich denke, die Art Sie wollen dies:

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

(Die #:- Klausel ist optional, ich eingeschlossen nur da es auf Vollständigkeit.)

Hinweis: Wenn die #:- Klausel ist enthalten, wird es nicht typecheck in Racket 6.1.1. Durch das Entfernen der Klausel wird es möglich sein, 6.1.1.

Das Problem hier ist, dass alle Zweige von case->unabhängig voneinander gegenseitig typen überprüfen müssen. Für den Fall (A -> A) schlägt es fehl, weil #f kein A ist. Das Auftreten von Tippinformationen aus dem ersten Fall kann die Typprüfung im zweiten Fall nicht beeinflussen.