racket contract dependency evaluation twice?

Question

#lang racket

(module inside racket
  (provide
    (contract-out
      [dummy (->i ([x       (lambda (x) (begin (displayln 0) #t))]
                   [y (x)   (lambda (y) (begin (displayln 1) #t))]
                   [z (x y) (lambda (z) (begin (displayln 2) #t))]
                   )
                  any
                  )]
      )
    )

  (define (dummy x y z) #t)
  )

(require 'inside)

(dummy 1 2 3)

The output is

0
0
1
1
2
#t

It's unclear to me why having x and y as dependencies would require the corresponding guard to fire again.

The doc of ->i http://docs.racket-lang.org/reference/function-contracts.html#%28form._%28%28lib.racket%2Fcontract%2Fbase..rkt%29.-~3ei%29%29 doesn't seem to mention this behavior.

Anyone can shed some light on this?

Answer 1

This was as confusing to me as it was to you, so I took the opportunity to ask this question on the Racket mailing list. What follows is an attempt to summarize what I found.

The ->i combinator produces a dependent contract that uses the indy blame semantics presented in the paper Correct Blame for Contracts. The key idea presented in the paper is that, with dependent contracts, there can actually be three parties that might need to be blamed for contract violations.

With normal function contracts, there are two potentially guilty parties. The first is the most obvious one, which is the caller. For example:

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

The second potential guilty party is the function itself; that is, the implementation might not match the contract:

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

Both of these cases are pretty obvious. However, the ->i contract introduces a third potential guilty party: the contract itself.

Since ->i contracts can execute arbitrary expressions at contract attachment time, it’s possible for them to violate themselves. Consider the following contract:

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

This is a somewhat silly contract, but it’s easy to see that it’s a naughty one. It promises to only call mk-ctc with integers, but the dependent expression (mk-ctc "hello") calls it with a string! It would obviously be wrong to blame the calling function, since it has no control over the invalid contract, but it might also be wrong to blame the contracted function, since the contract could be defined in complete isolation from the function it is attached to.

For an illustration of this, consider a multi-module example:

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

In this example, the ctc contract is defined in the m1 submodule, but the function that uses the contract is defined in a separate submodule, m2. There are two possible blame scenarios here:

1. The foo function is obviously invalid, since it applies f to #f, despite the contract specifying (integer? . -> . integer?) for that argument. You can see this in practice by calling 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)

   I’ve emphasized the spot in the contract error that includes blame information, and you can see that it blames m2, which makes sense. This isn’t the interesting case, since it’s the second potential blame party mentioned in the non-dependent case.

2. However, the ctc contract is actually a little bit wrong! Note that the contract on v applies f to v, but it never checks that v is an integer. For this reason, if v is something else, f will be called in an invalid way.¹ You can see this behavior by giving a non-integral value for 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)

   The top of the contract error is the same (Racket provides the same “broke its own contract” message for these kinds of contract violations), but the blame information is different! It now blames m1, which is the actual source of the contract. This is the indy blame party.

This distinction is what means the contracts have to be applied twice. It applies them with each distinct blame party’s information: first it applies them with the contract-blame, then it applies them with the function-blame.

Technically, this could be avoided for flat contracts, since flat contracts will never signal a contract violation after the initial contract attachment process. However, the ->i combinator currently does not implement any such optimization, since it probably wouldn’t have a significant impact on performance, and the contract implementation is already fairly complex (though if someone wanted to implement it, it would likely be accepted).

In general, though, contracts are expected to be stateless and idempotent (flat contracts are expected to be simple predicates), so there’s not really any guarantee that this won’t happen, and ->i just uses that to implement its fine-grained blame information.

---

^{1. As it turns out, the ->d contract combinator doesn’t catch this issue at all, so add1 ends up raising a contract violation here. This is why ->i was created, and it’s why ->i is favored over ->d.}