[plt-scheme] mutual recursion in contracts

> Recursive ho contracts gets tricky. I'm not sure how to do them in the
> general case, either.

I'm just learning about contracts so I don't know what all the issues 
are (aside from some of the obvious undecidability problems), but I 
believe you that it's hard. In my case I might be okay with just 
disallowing h.o. contracts.

> Perhaps if you supply some detail of the particular contracts I can
> suggest something or maybe add something to the library to help.

The most useful form, I think, would be define-struct/contract. I'm 
writing an algebraic datatype form like EoPL's define-datatype, but 
made to work with your contract system. (It's implemented with 
define-struct and subtyping.) In order to be consistent with similar 
forms in the contract library, it currently separates definition from 
attaching contracts, e.g.:

   (define-datatype expr
     [var-expr (name)]
     [lam-expr (var body)]
     [app-expr (rator rand)])
   (provide-datatype/contract expr
     [var-expr (string?)]
     [lam-expr (string? expr?)]
     [app-expr (expr? expr?)])

But I'd like to be able to attach contracts to a datatype at the point 
of definition. This is where problems with mutual recursion come in. To 
cook up an example, imagine writing a compiler for some sort of 
first-order imperative language:

   (define-datatype/contract type ...)
   (define-datatype/contract decl
     [proc-decl ([name string?]
                 [return-type type?]
                 [formals (listof (cons/p string? type?))]
                 [body expr?])]   ;; <-- refers to expr
     [var-decl  ([name string?]
                 [type type?]
                 [init expr?])])
   (define-datatype/contract expr
     [let-expr  ([decl var-decl?] ;; <-- refers to var-decl
                 [body expr?])]
     [call-expr ([proc string?]
                 [operands (listof expr?)])]
     ...)

There are two problems with implementing a define-datatype/contract 
macro. First of all, the contracts currently can't be attached to 
structs except in provide forms. So define-struct/contract would be 
helpful. The second problem is how to implement the mutual recursion in 
the contracts. I suppose if I stuck with flat contracts and predicates, 
then I could just eta-expand all the contract expressions.

Incidentally, I'm curious about the claim in your ICFP paper that 
contracts are most useful at module boundaries. The libraries don't 
even always support the use of contracts within the module in which 
they're defined. In my case it seems like it would be useful to be able 
to define local datatypes that aren't exported but whose contracts are 
enforced within the same module.

Anyway, sorry for the long email and thanks as always for your time.

Dave