球拍 - 函数参数的合同可以依赖于另一个参数的值吗？

Question

假设我有一个函数：

(define (func x y)
    ...)

我想限制参数，以便：

• x 是一个正整数
• y 是小于或等于 x 的正整数

第一个约束显然是微不足道的，但是有什么办法可以用 Racket 的合约系统设置第二个约束？

Answer 1

是的。您想使用 依赖合约，在 Racket 中使用 ->i 合约组合器表示。您所描述的函数的合同如下所示：

(->i ([x (and/c integer? positive?)]
      [y (x) (and/c integer? positive? (<=/c x))])
     [result any/c])

以下是不当应用与上述合同约定的功能时会发生的错误类型的示例：

> (func 1 2)
func: contract violation
  expected: (and/c integer? positive? (<=/c 1))
  given: 2
  in: the y argument of
      (->i
       ((x (and/c integer? positive?))
        (y
         (x)
         (and/c integer? positive? (<=/c x))))
       (result any/c))
  contract from: (function func)

对于依赖合约，所有参数和结果都需要命名，以便在其他子句中引用。第二个参数子句中的(x) 指定y 的合约取决于 x 的值，因此您可以在y 的合约规范中使用x。

->i 的完整语法可在 in the documentation 获得，它有很多附加功能。它也有一些示例，包括与您问题中的示例非常相似的示例。