如何在类型化球拍中使用定义/合同(或类似的内容)？

Question

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

我想写

#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))

但是类型化的Racket不提供自己的define/contract，而vanilla define/contract也不理解类型化的Racket的注释(它引发语法错误)。

我能设法解决这个问题吗？我可以使用裸contract以define/contract的方式将合同附加到excited-logarithm吗？

而且，我不该这么做有什么好的理由吗？是否不鼓励合同和类型的混合？

注意:我想我真正想要的是依赖式输入，但在Racket中是没有的。

Answer 1

这里的简单答案是:使用“非负-真实”类型，或者其他类似的TR类型来捕捉这个想法。

.Positive-.Real%29%29

(这里也有细化类型，但您不需要它们。)