Typed Racket命题出现奇怪的类型不匹配错误

Question

我正在Typed Racket中尝试命题，并得到了一个以前从未见过的类型错误，我对此一无所知。

示例代码：

#lang typed/racket/base
(require racket/fixnum)
; Version of fx= that takes two or more arguments (The TR version only takes 2)
(: fx=? (Fixnum Fixnum Fixnum * -> Boolean))
(define (fx=? a b . nums)
(and (fx= a b)
(andmap (lambda ([c : Fixnum]) (fx= a c)) nums)))
(: fxzero? (Fixnum -> Boolean : Zero))
(define (fxzero? i) (fx=? i 0))

试图编译这个给出：

demo.rkt:12:20: Type Checker: type mismatch;
mismatch in proposition
expected: ((: i Zero) | (! i Zero))
given: (Top | Top)
in: (fx=? i 0)
compilation context...:

使用=或fx=将按预期编译和工作，fx=?函数在其他地方也可用。删除: Zero命题使它也可以编译和工作。

该错误消息中的预期类型和给定类型不在我以前见过的注释中，在文档中也找不到提及它的内容。有人以前见过它，或者可以解释我的fx=?与其他破坏我的fxzero?的功能相比有什么不同？

Answer 1

我认为这里的第一个也是最大的问题是，应用于fx=?函数的类型没有任何命题，因此使用它的函数将无法推断出它在内部的操作方式。话虽如此，我认为你将花大量时间来制定一个适用于fx=?函数的有用命题。具体来说，你要求TR通过andmap类型表演一些极其复杂的杂技。

换句话说：当你制定这样的命题时，我声称TR不会去探索和尝试证明你的代码。相反，发生类型意味着有可能向上传播信息，如果这些信息可以用命题来表达，如果这些命题可以粘在一起得到你想要的结果。在参数列表中包含*的类型上，命题似乎也是不允许的。

以防万一，这并不明显；你知道这个程序类型检查得很好，对吧？：

#lang typed/racket/base
(require racket/fixnum)
(: fxzero? (Fixnum -> Boolean : Zero))
(define (fxzero? i) (fx= i 0))