在Typed Racket中表示函数EOF -> False, A -> A ∀ A ≠ EOF？

Question

我正在尝试为 Typed Racket 中的以下函数定义类型注释：

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

不加注释给出类型：

(Any -> Any)

使用此类型会产生错误：

(: 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 或端口的值。我现在正在重新考虑是否需要这样做，因为我花了太多时间试图找出这种类型。

为了完整起见，我还尝试了 neof 的定义：

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

（第二个模式也是 _，但它没有编码相同数量的类型信息。在这一点上，我更想安抚类型检查器而不是任何东西）。

所以：我如何表示 neof 的类型？

Answer 1

我想你想要的类型是这样的：

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

（#:- 子句是可选的，为了完整起见，我只是将其包含在那里。）

注：如果包含#:-子句，则不会 Racket 6.1.1 中的类型检查。删除条款将允许它通过 6.1.1.

这里的问题是 case-> 的所有分支都必须 独立地 进行类型检查。对于 (A -> A) 的情况，它失败了，因为 #f 不是 A。第一种情况的出现类型信息不会影响第二种情况的类型检查。

Representing the function EOF -> False, A -> A ∀ A ≠ EOF in Typed Racket?