在键入的球拍中表示功能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. 第一种情况的出现类型信息不会影响第二种情况的类型检查。