Я пишу небольшой проект в Racket и использую библиотеку Грегор для обработки дат.
У меня есть функция, которая принимает две даты (от Грегора, а не из стандартной библиотеки), и я хотел бы добавить для нее контракт. В контракте должно быть указано, что дата первого аргумента должна быть меньше/раньше, чем дата второго аргумента.
В Грегоре мы можем добиться этого, используя (дата <=? х г) или аналогичный предикат, но я не могу понять, как это совместить с контрактами.
(contract-out
[process-dates (->i ([x date?]
[y (x) (and/c date?
(date>=? x))])])
не будет работать, и нет предиката date>=?/c из коробки.
Поэтому я предполагаю, что мне нужно будет написать такие предикаты самостоятельно, поэтому я хотел бы знать, как это сделать. Я просмотрел исходники Racket и обнаружил, что стандартные функции — это довольно сложный для воспроизведения.
Есть ли более простой способ добиться того, чего я хочу?

Самый простой способ — использовать lambda:
(->i ([x date?]
[y (x) (and/c date? (lambda (y) (date>=? y x)))])
[_ any/c])
Одним из недостатков является то, что в случае нарушения контракта сообщение об ошибке будет содержать ??? вместо лямбда-выражения. Если вы хотите, чтобы он напечатал там что-то более значимое, вы можете сделать что-то вроде следующего:
(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.
Хотя ответ Райана великолепен, я обнаружил, что эту проблему можно решить следующим образом, используя предварительное условие:
(->i ([x date?]
[y date?])
#:pre (x y) (date<=? x y)
;; ...
)
Идеально! Сообщение об ошибке действительно не очень полезно, но что касается Racket7.3, по крайней мере, я вижу лямбда-выражение в трассировке.