оценка зависимости от контракта с ракеткой дважды?

Это сбивало меня с толку так же, как и вас, поэтому я воспользовался возможностью, чтобы задайте этот вопрос в списке рассылки Racket. Далее следует попытка обобщить то, что я обнаружил.

Комбинатор ->i создает зависимый контракт, который использует семантику indy blame, представленную в документе Правильное определение виновности для контрактов. Ключевая идея, представленная в документе, заключается в том, что в случае зависимых контрактов на самом деле могут быть три стороны, которых, возможно, придется обвинить в нарушении контрактов.

В обычных функциональных контрактах есть две потенциально виновные стороны. Первый из них наиболее очевиден - это вызывающий абонент. Например:

> (define/contract (foo x)
    (integer? . -> . string?)
    (number->string x))
> (foo "hello")
foo: contract violation
  expected: integer?
  given: "hello"
  in: the 1st argument of
      (-> integer? string?)
  contract from: (function foo)
  blaming: anonymous-module
   (assuming the contract is correct)

Вторая потенциальная виновная сторона - это сама функция; то есть реализация может не соответствовать контракту:

> (define/contract (bar x)
    (integer? . -> . string?)
    x)
> (bar 1)
bar: broke its own contract
  promised: string?
  produced: 1
  in: the range of
      (-> integer? string?)
  contract from: (function bar)
  blaming: (function bar)
   (assuming the contract is correct)

Оба эти случая довольно очевидны. Однако ->i контракт вводит третью потенциальную виновную сторону: сам контракт.

Поскольку ->i контракты могут выполнять произвольные выражения во время прикрепления контракта, они могут нарушать себя. Рассмотрим следующий договор:

(->i ([mk-ctc (integer? . -> . contract?)])
      [val (mk-ctc) (mk-ctc "hello")])
     [result any/c])

Это несколько глупый контракт, но легко понять, что он непристойный. Он обещает вызывать mk-ctc только с целыми числами, но зависимое выражение (mk-ctc "hello") вызывает его со строкой! Очевидно, было бы неправильно винить вызывающую функцию, поскольку она не контролирует недействительный контракт, но может быть также неправильно обвинять контрактную функцию, поскольку контракт может быть определен в полной изоляции от функция, к которой он прикреплен.

Чтобы проиллюстрировать это, рассмотрим многомодульный пример:

#lang racket

(module m1 racket
  (provide ctc)
  (define ctc
    (->i ([f (integer? . -> . integer?)]
          [v (f) (λ (v) (> (f v) 0))])
         [result any/c])))

(module m2 racket
  (require (submod ".." m1))
  (provide (contract-out [foo ctc]))
  (define (foo f v)
    (f #f)))

(require 'm2)

В этом примере контракт ctc определен в подмодуле m1, но функция, использующая контракт, определена в отдельном подмодуле m2. Здесь есть два возможных сценария обвинения:

1. Очевидно, что функция foo недействительна, поскольку она применяет f к #f, несмотря на то, что контракт определяет (integer? . -> . integer?) для этого аргумента. Вы можете увидеть это на практике, позвонив foo:

   > (foo add1 0)
   foo: broke its own contract
     promised: integer?
     produced: #f
     in: the 1st argument of
         the f argument of
         (->i
          ((f (-> integer? integer?))
           (v (f) (λ (v) (> (f v) 0))))
          (result any/c))
     contract from: (anonymous-module m2)
     blaming: (anonymous-module m2)
      (assuming the contract is correct)

   Я выделил место в контракте с ошибкой, которое включает информацию об обвинении, и вы можете видеть, что он обвиняет m2, что имеет смысл. Это не интересный случай, поскольку это вторая потенциальная виновная сторона, упомянутая в независимом деле.

2. Однако контракт ctc на самом деле немного неправильный! Обратите внимание, что контракт на v применяет f к v, но никогда не проверяет, является ли v целым числом. По этой причине, если v - это что-то еще, f будет вызываться недопустимым способом. ¹ Вы можете увидеть это поведение, указав нецелое значение для v:

   > (foo add1 "hello")
   foo: broke its own contract
     promised: integer?
     produced: "hello"
     in: the 1st argument of
         the f argument of
         (->i
          ((f (-> integer? integer?))
           (v (f) (λ (v) (> (f v) 0))))
          (result any/c))
     contract from: (anonymous-module m1)
     blaming: (anonymous-module m1)
      (assuming the contract is correct)

   Верхняя часть ошибки контракта такая же (Racket предоставляет такое же сообщение «нарушил свой собственный контракт» для такого рода нарушений контракта), но информация о виновности другая! Теперь он обвиняет m1, который является фактическим источником контракта. Это инди виноват.

Это различие означает, что контракты должны применяться дважды. Он применяет их к информации каждой отдельной виновной стороны: сначала он применяет их к контракту-обвинению, затем он применяет их к функции-виноватому.

Технически этого можно было бы избежать для плоских контрактов, поскольку плоские контракты никогда не будут сигнализировать о нарушении контракта после первоначального процесса присоединения контракта. Однако комбинатор ->i в настоящее время не реализует такую ​​оптимизацию, поскольку она, вероятно, не окажет значительного влияния на производительность, а реализация контракта уже довольно сложна (хотя, если кто-то захочет реализовать ее, она, вероятно, будет принята).

Однако в целом ожидается, что контракты не будут иметь состояния и будут идемпотентными (предполагается, что плоские контракты будут простыми предикатами), поэтому на самом деле нет никакой гарантии, что это не произойдет, и ->i просто использует это для реализовать его детализированную информацию о виновности.

^{1. Оказывается, комбинатор контрактов ->d вообще не улавливает эту проблему, поэтому add1 в конечном итоге вызывает нарушение контракта. Вот почему был создан ->i, и поэтому ->i предпочтительнее ->d.}