[plt-scheme] Questions about (contract ...) form

From: Robby Findler (robby at cs.uchicago.edu)
Date: Sun Nov 6 16:10:01 EST 2005

Overall, I suspect the problem is that we don't have a good story for
contracts+macros. Sounds like a nice research topic to me!

To avoid the problem and make progress, just stick a dynamic check into
the expansion of the stream-cons macro and move on.


At Sun, 6 Nov 2005 16:04:43 -0500, Richard Cobbe wrote:
> On Sun, Nov 06, 2005 at 02:32:35PM -0600, Robby Findler wrote:
> > At a high level `contract' is used as the definition of some kind of
> > boundary between "things". In the case of provide/contract (which
> > expands to contract), the things are modules. In the case of
> > define/contract, the things are definitions (but define doesn't work as
> > well as a module leading to some strange things with define/contract
> > sometimes ... but that's neither here nor there). So the first question
> > to answer is what the "things" are.
> In this case, they're modules.  I could have made this clearer by
> describing more of the context.  Here's what I've got currently:
> (module ministream mzscheme
>   (require (lib "contract.ss"))
>   (define-struct stream ())
>   (define-struct (stream:empty stream) ())
>   (define-struct (stream:cell stream) (car cdr))
>   (define-syntax stream-cons
>     (syntax-rules ()
>       [(_ a d)
>        (make-stream:cell a (delay d))]))
>   (define stream-car
>     (lambda (str)
>       (if (stream:empty? str)
>           (raise (make-exn:fail:contract
>                   "can't take car of empty stream"
>                   (current-continuation-marks)))
>           (stream:cell-car str))))
>   (define stream-cdr
>     (lambda (str)
>       (if (stream:empty? str)
>           (raise (make-exn:fail:contract
>                   "can't take cdr of empty stream"
>                   (current-continuation-marks)))
>           (force (stream:cell-cdr str)))))
>   (define stream-null (make-stream:empty))
>   (define stream-null? stream:empty?)
>   (provide stream-cons)
>   (provide/contract [stream? (-> any/c boolean?)]
>                     [stream-car (-> stream? any)]
>                     [stream-cdr (-> stream? stream?)]
>                     [stream-null stream?]
>                     [stream-null? (-> stream? boolean?)]))
> But I've discovered that blame doesn't get assigned the way I think it
> should.  If some other module does the following:
>     (stream-cdr (stream-cons 3 4))
> then ministream gets blamed for violating stream-cdr's contract.  That's
> what I've written, of course, but that's not what I want --- it's not
> ministream's fault, it's the client's fault for constructing a bogus
> stream in the first place.  Ideally, the contract system would blame the
> client for violating stream-cons's contract; I just can't figure out how
> to write that contract.
> Basically, I'm trying to figure out how to do this
>     (provide/contract [stream-cons (-> any/c stream? stream?)])
> given that stream-cons has to be a macro.  (Actually, I don't really
> care about the contract on stream-cons's return value; I'm confident
> that I got that right.  <grin>)
> > >   b) Is negative-blame meaningful when the value in question is not a
> > >      function?
> > 
> > Yes. The contract language is set up so that each contract should be
> > between two parties (this also works for N parties, when you think of
> > N+1 pairwise contracts with some common one "thing" that connects them
> > together -- if you need something like that directly we can talk more
> > about it.). One party is responsible the value initially and things
> > that flow in the first direction (positive) and the other is
> > responsible for values that flow back into the original place. So, in
> > the case of functions, positive is for the function itself (it's arity)
> > and for results of the function. Negative is for arguments to the
> > function (or results of argument functions, etc).
> OK.  I'm not quite sure how this applies to my situation.  I know one of
> the two symbols will be 'ministream and the other will be the client
> module, but I'm not sure which is which.  Based on what you say above,
> it sounds like the client module should be the negative blame, because
> it's (kind of) a function argument, but I'm not at all sure about that.
> More generally, I don't completely understand the forward and backward
> directions.  There's an obvious relation to positive and negative
> positions here, but it looks like it's more complex than that.
> > But there are other kinds of connections between "things" (beyond
> > functions) that allow backwards flow.
> > 
> > >   c) If these symbols are supposed to be module names, how do I get the
> > >      name of the module which contains the use of stream-cons?  I've
> > >      seen syntax-source-module, but that can potentially return a module
> > >      path index, and it's not clear how to extract the module name from
> > >      that.
> > 
> > See module-source-as-symbol in mzlib/private/contract-helpers for what
> > provide/contract does.
> Thanks for the pointer; I'll check that out.
> > > Second, the manual says that "contract-source, if specified, indicates
> > > where the contract was assumed."  What does it mean to assume a
> > > contract?
> > 
> > Assume as in "to take it on", not assume as in "prove an implication".
> I'd sort of figured that was what you meant, but it's still not clear to
> me what it means to "take on" a contract.  Wild guess: is this a way of
> making it appear as though the contract was applied to the value in one
> module even though the actual contract form appears somewhere else?  For
> instance, I'd guess that provide/contract uses that to make the contract
> look as though it comes from the use of provide/contract, not its
> definition.  If that's the case, then, I could just use the default, as
> I'd like the contract to appear as though it comes from ministream.
> > > Or is there a better way to do this altogether?
> > 
> > I guess provide/contract doesn't work for you because you want to
> > export a macro?
> Yup.
> Richard
> _________________________________________________
>   For list-related administrative tasks:
>   http://list.cs.brown.edu/mailman/listinfo/plt-scheme

Posted on the users mailing list.