[plt-scheme] Attaching contracts to unit exports
On 3/2/07, Paulo J. Matos <pocm at soton.ac.uk> wrote:
> > If you wanted to explore doing that, you'd probably want to use
> > `contract' directly, but that form requires you to give names for
> > blame assignment.
> >
>
Well, I went to read the PLT Scheme MzLib manual and on the 'contract'
it says among other things:
"The expressions positive-blame and negative-blame must be symbols
indicating how to assign blame for positive and negative positions of
the contract specified by contract-expr."
I was not able to understand what positive/negative blame was but I
guessed it had to do with whom to blame and a symbol would be enough.
I could pass something like 'foo and 'bar and then using some internal
algorithm it would blame either foo or bar. Anyway, semantically that
meant nothing to me which took me to your ICFP02 paper where in
section 2.3 you say and I quote:
"Unlike first-order function contract checking, a more general rule
applies for blame assignment. The rule is based on the number of times
that each base contract appears to the left of an arrow in the
higher-order contract. If the base contract appears an even number of
times, the function itself is responsible for establishing the
contract. If it appears an odd number of times, the function's caller
is responsible."
Well, this stroke me hard. First I got confused with even/odd in paper
and positive/negative in manual, is there any equivalence between
these?
Moreover, what do you mean by base contract and why this rule works? I
can't find this anywhere else and I can't understand through the
following example why it works.
By examining the example:
(define/contract g
((greater-than-nine? . -> . between-zero-and-ninety-nine?) . -> .
between-zero-and-ninety-nine?)
(lambda (f) (f 0)))
Are the base contracts : greater-than-ninety-nine? and
between-zero-and-ninety-nine? ?
If yes, then greater-than-ninety-nine? appears once and
between-zero-and-ninety-nine? appears twice but still, when finding
the blame for the failing of greater-than-nine? you say in the paper
that it is g fault. I understand it is g fault but the rule seems to
say otherwise (obviously I'm missing something), because it say that
when it appears an odd number of times the blame is on the functions
caller, so the one who called g and passed f in should be blamed.
Back to PLT Scheme, how can I relate this rule to the positive and
negative blame arguments?
Sorry for the big, probably full of non-sense email,
--
Paulo Jorge Matos - pocm at soton.ac.uk
http://www.personal.soton.ac.uk/pocm
PhD Student @ ECS
University of Southampton, UK