Reprezentowanie funkcji EOF -> Fałsz, A -> A ∀ A ≠ EOF w typowanej rakiecie?

Question

Próbuję określić adnotacji typu dla następujących funkcji w Typed Racket:

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

pozostawiając ją un-uwagami daje typ:

(Any -> Any) 

korzystania z tego typu generuje błąd:

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

    expected: A 
    given: False 
    in: #f 

Jest to prawdopodobnie dlatego, że można pozwolić A = EOF, a następnie otrzymujemy EOF -> EOF.

Typ (: neof (All (A) A -> (U A False) #:- (U EOF False))), choć nie tak oczywiste, jak wyżej, daje również błędy:

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

Moim celem było mieć funkcję, która mógłbym zastosować do dowolnego wyjścia z portu uzyskać albo False lub temu wartość z portu. Teraz zastanawiam się nad potrzebą tego, ponieważ zbyt dużo czasu spędziłem próbując dojść do tego typu.

Dla kompletności, próbowałem również tę definicję neof.

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

(również drugi wzór jest _, ale które nie kodują tę samą ilość informacji typu W tym momencie jestem bardziej próbuje uspokoić sprawdzanie typu niż cokolwiek innego).

Więc: w jaki sposób mogę reprezentować typ neof?

Answer 1

myślę typ chcesz to:

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

(Klauzula #:- jest opcjonalny, po prostu wliczone jest tam dla kompletności.)

Uwaga: Jeśli klauzula #:- jest włączone, będzie to nie typecheck w Rakiecie 6.1.1. Usunięcie tej klauzuli pozwoli jej przekazać 6.1.1.

Problem polega na tym, że wszystkie oddziały należące do case-> muszą samodzielnie odczytywać niezależnie. Dla przypadku (A -> A) nie działa, ponieważ #f nie jest A. Wystąpienie wpisywania informacji z pierwszego przypadku nie może wpływać na sprawdzanie typu w drugim przypadku.