[plt-scheme] Attaching contracts to unit exports

On Mar 2, 2007, at 10:07 AM, Paulo J. Matos wrote:

> 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."

The negative position is the left side of the arrow. The positive  
position is the right side of the arrow.  Since these positions can  
themselves be arrow types, you can talk about the positive position  
of a negative position.  In this example

((a -> b) -> (c -> d))

The letter 'b' occurs in the positive position of a negative  
position.  The letter 'c' appears in the negative position of a  
positive position.

The distinction here is on how many "negative links" you have to  
follow to get to the given type.  In this type, 'b' and 'c' both  
require following one negative link. That means that the function's  
caller is responsible, since one is an odd number.  'a' requires  
following two negative links.  Two is an even number, so the function  
itself is responsible .  'd' requires following zero negative links,  
so again the function itself is responsible.

Corrections welcome,

John

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2484 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20070302/ac4a6bbe/attachment.p7s>