Presentation of the EOF Function & # 8594; False, A & # 8594; A ∀ A ≠ EOF in a typed racket?

Question

I am trying to define type annotation for the following function in Typed Racket:

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

If you leave it unannotated, enter the type:

 (Any -> Any) 

Using this type creates an error:

 (: neof (All (A) (case-> (EOF -> False) (A -> A : #:+ (! EOF)))) expected: A given: False in: #f 

This is apparently because we can enable A = EOF , and then we get EOF -> EOF .

Type (: neof (All (A) A -> (UA False) #:- (U EOF False))) , although not as clear as above, also gives errors:

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

My goal was to have a function that I could apply to any output from the port, get either False or a value from the port. Now I am redefining the need for this, as I have been trying to figure out this type for too long.

For completeness, I also tried this definition of neof :

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

(Also with the second pattern is _ , but it does not encode the same amount of type information. At this point I am trying more to calm type checking than anything).

So: how can I represent a type of neof ?

Answer 1

I think the type you want is this:

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

(Suggestion #:- optional, I just included it for completeness.)

Note. If clause #:- included, it will not be checked in Racket 6.1.1. Deleting an offer will allow him to go through 6.1.1.

The problem here is that all case-> branches should be marked independently. For the case (A -> A) it fails because #f not A Data entry information from the first case cannot affect type checking in the second case.