如何在 Typed Racket 中使用定义/合同（或类似的东西）？答案

【问题标题】：How can I use define/contract (or something equivalent) in Typed Racket?如何在 Typed Racket 中使用定义/合同（或类似的东西）？
【发布时间】：2017-10-29 14:59:30
【问题描述】：

我正在编写一个只接受正数的函数，我想确保它在模块内部和其他地方都能正确使用。

我想写

#lang typed/racket
(require racket/contract)

(: excited-logarithm (-> Number Number))
(define/contract (excited-logarithm ([x : Number]) : Number)
  (-> (>=/c 0) number?)
  (displayln "Hold on to your decimals, we're going in!")
  (log x))

但是 Typed Racket 不提供自己的 define/contract，而原版 define/contract 不理解 Typed Racket 的注释（它会引发语法错误）。

我能以某种方式解决这个问题吗？我可以像define/contract 那样使用裸contract 将合同附加到excited-logarithm 吗？

此外，我不应该这样做有充分的理由吗？不鼓励混合合约和类型？

注意：我想我在这里真正想要的是依赖类型，但这在 Racket 中不可用。

【问题讨论】：

标签： racket contract typed-racket

【解决方案1】：

这里的简单答案：使用“Nonnegative-Real”类型，或捕捉此想法的其他类似 TR 类型之一。

http://docs.racket-lang.org/ts-reference/type-ref.html?q=Positive-Real#%28form._%28%28lib.typed-racket%2Fbase-env%2Fbase-types..rkt%29..Positive-.Real%29%29

（这里也有细化类型，但你不需要它们。）

【讨论】：

哇，我在参考中错过了这些，谢谢！但是，对于一般情况，问题仍然存在。
这取决于你的“一般”情况有多普遍。您可以使用细化类型来捕获一些这样的约束，当然您也可以定义自己的简单平面合约宏来执行此检查；合约中大部分有趣/具有挑战性的部分都发生在函数类型上。
什么是“细化类型”？我在 Typed Racket 文档中搜索了该术语，但没有找到任何内容。
对于不存在特定类型的一般情况，intersection types 可能是一种可能性。
@ssdecontrol 这是 6.10 中的“实验性功能”。这是文档的 URL：docs.racket-lang.org/ts-reference/…