Racket：在合同中使用的自定义谓词答案

【问题标题】：Racket: Custom predicate to use within contractRacket：在合同中使用的自定义谓词
【发布时间】：2019-06-25 11:21:40
【问题描述】：

我正在用 Racket 编写小型宠物项目，并使用 Gregor lib 来处理日期。

我有接受两个日期的函数（来自 Gregor，而不是标准库），我想为它添加合同。合同应该说第一个参数的日期必须小于/早于第二个参数的日期。

在 Gregor 我们可以使用(date<=? x y) 或类似的谓词来实现它，但我不明白如何将它与合约结合起来。

 (contract-out
          [process-dates (->i ([x date?]
                               [y (x) (and/c date?
                                             (date>=? x))])])

将不起作用，并且没有开箱即用的 date>=?/c 谓词。

所以我想我需要自己编写这样的谓词，因此我想知道该怎么做。我查看了 Racket 的源代码，发现标准功能是 quite complicated 可以重现。

有没有更简单的方法来实现我想要的？

【问题讨论】：

标签： date scheme racket predicate contract

【解决方案1】：

最简单的方法是使用lambda：

(->i ([x date?]
      [y (x) (and/c date? (lambda (y) (date>=? y x)))])
     [_ any/c])

一个缺点是，如果违反合同，错误消息将包含??? 代替 lambda 表达式。如果您希望它在那里打印更有意义的内容，您可以执行以下操作：

(define (date>=/c x)
  (flat-named-contract
   `(date>=/c ,x)
   (lambda (y) (date>=? y x))))
....
(->i ([x date?]
      [y (x) (and/c date? (date>=/c x))])
     [_ any/c])

如果您想更好地控制错误消息，可以尝试使用flat-contract-with-explanation。

【讨论】：

完美！错误信息确实不是很有用，但是对于 Racket7.3 至少我可以在 trace 中看到 lambda 表达式。

【解决方案2】：

虽然 Ryan 的回答很棒，但我发现可以通过以下方式解决这个问题，使用前提条件：

(->i ([x date?]
      [y date?])
    #:pre (x y) (date<=? x y)
    ;; ...
 )

【讨论】：