为什么 Typed Racket 认为 `cond` 可以在这里返回 `Void`？

【问题标题】：Why does Typed Racket think that `cond` can return `Void` here?为什么 Typed Racket 认为 `cond` 可以在这里返回 `Void`？
【发布时间】：2022-12-19 14:15:33
【问题描述】：

Typed Racket 似乎认为这个条件可以返回Void。为什么？

#lang typed/racket

(define x : Real 1234)

(+ 4 (cond [(< x 5) 5]
           [(<= 5 x) 10]))

...产生错误

Type Checker: type mismatch
  expected: Number
  given: (U Positive-Byte Void) in: (cond ((< x 5) 5) ((<= 5 x) 10))

为什么？

【问题讨论】：

标签： typed-racket

【解决方案1】：

这里的问题是，由于历史原因，当所有测试子句都失败时，cond 将返回 (void) 值。看着这段代码，您可能会说“但是等等！那是不可能的！每个实数都必须是 (< 5) 或 (>= 5)，对吗？”好吧，这是真的，但这不是 Typed Racket 可以在其类型系统范围内推理的东西。

所以你会怎么做？好吧，在这种情况下，使用 Typed Racket 分享您的知识非常容易。只需将最后一个测试更改为 else 子句，TR 可以看到该子句必须始终成功：

#lang typed/racket

(define x : Real 1234)

(+ 4 (cond [(< x 5) 5]
           [else 10]))

... 类型检查并运行良好。

【讨论】：