[plt-dev] Re: [plt-scheme] New contract-related features

Note that you get the same error message if you do this:

> (define (f x)
 (define y x))
. begin (possibly implicit): no expression after a sequence of
internal definitions in: ((define y x))

Do you think `with-contract' should give a special error message here,
or that the error message in general should be improved?

sam th

On Sun, Feb 15, 2009 at 2:24 PM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
>
> Could we improve the error message for people who attempt to nest regions
>
>> #lang scheme
>>
>> (with-contract f1
>>               ((y number?))
>>               (with-contract f2
>>                              ((x boolean?))
>>                              (define x #t)
>>                              (define y 1)))
>>
>
> or
>
>> #lang scheme
>>
>> (define (f x)
>>  (with-contract
>>   f1
>>   ((y number?))
>>   (define y x)))
>>
>> (f 10)
>
> Thanks. -- Matthias
>
>
>
> On Feb 14, 2009, at 11:24 PM, Stevie Strickland wrote:
>
>> In SVN I've added three new major features that involve contracts.
>> One allows for more fine-grained control of contracts, and the other
>> two allow for the use of contracts with signatures and units.
>>
>> Contract Regions
>> ----------------
>>
>> Contract regions allow the programmer to protect a region of code
>> with a contract boundary.  In addition to the wrapped code, the
>> programmer also provides a name for the region which is used in
>> blame situations and a list of exported variables which can
>> either be protected with contracts or unprotected.  The region
>> provides a true contract boundary, in that uses of contracted
>> exports within the region are unprotected.  Contract regions are
>> specified with the with-contract form.  The following contract
>> region defines two mutually recursive functions:
>>
>>  (with-contract region1
>>    ([f (-> number? boolean?)]
>>     [g (-> number? boolean?)])
>>    (define (f n) (if (zero? n) #f (g (sub1 n))))
>>    (define (g n) (if (zero? n) #t (f (sub1 n)))))
>>
>> The internal calls to f and g are uncontracted, but calls to f
>> and g outside this region would be appropriately contracted.
>> First-order checks are performed at the region, so the
>> following region:
>>
>>  (with-contract region2
>>    ([n number?])
>>    (define n #t))
>>
>> results in the following error:
>>
>>  (region region2) broke the contract number? on n;
>>    expected <number?>, given: #t
>>
>> Notice that the blame not only gives the name of the region, but
>> describes what type of contract boundary was involved.
>>
>> For contracting a single definition, there is the define/contract
>> form which has a similar syntax to define, except that it takes a
>> contract before the body of the definition.  To compare the two
>> forms, the following two definitions are equivalent:
>>
>> (with-contract fact
>>  ([fact (-> number? number?)])
>>  (define (fact n)
>>    (if (zero? n) 1 (* n (fact (sub1 n))))))
>>
>> (define/contract (fact n)
>>  (-> number? number?)
>>  (if (zero? n) 1 (* n (fact (sub1 n)))))
>>
>> First order checks are similarly performed at the definition for
>> define/contract, so
>>
>>  (define/contract (fact n)
>>    (-> number?)
>>    (if (zero? n) 1 (* n (fact (sub1 n)))))
>>
>> results in
>>
>>  (function fact) broke the contract (-> number?) on fact;
>>     expected a procedure that accepts no arguments without
>>     any keywords, given: #<procedure:fact>
>>
>> Signature Contracts
>> -------------------
>>
>> In addition to contract regions, units are also now contract
>> boundaries.  One way to use contracts with units is to add
>> contracts to unit signatures via the contracted signature form.
>>
>>  (define-signature toy-factory^
>>    ((contracted
>>      [build-toys (-> integer? (listof toy?))]
>>      [repaint    (-> toy? symbol? toy?)]
>>      [toy?       (-> any/c boolean?)]
>>      [toy-color  (-> toy? symbol?)])))
>>
>> Notice that contracts in a signature can use variables listed
>> in the signature.
>>
>> Now if we take the following implementation of that signature:
>>
>>  (define-unit simple-factory@
>>    (import)
>>    (export toy-factory^)
>>
>>    (define-struct toy (color) #:transparent)
>>
>>    (define (build-toys n)
>>      (for/list ([i (in-range n)])
>>        (make-toy 'blue)))
>>
>>    (define (repaint t col)
>>      (make-toy col)))
>>
>> We get the appropriate contract checks on those exports:
>>
>>  > (define-values/invoke-unit/infer simple-factory@)
>>  > (build-toys 3)
>>  (#(struct:toy blue) #(struct:toy blue) #(struct:toy blue))
>>  > (build-toys #f)
>>  top-level broke the contract (-> integer? (listof toy?))
>>    on build-toys; expected <integer?>, given: #f
>>
>> As before, uses of contracted exports inside the unit are
>> not checked.
>>
>> Since units are contract boundaries, they can be blamed
>> appropriately.  Take the following definitions:
>>
>>  (define-unit factory-user@
>>    (import toy-factory^)
>>    (export)
>>    (let ([toys (build-toys 3)])
>>      (repaint 3 'blue)))
>>
>>  (define-compound-unit/infer factory+user@
>>    (import) (export)
>>    (link simple-factory@ factory-user@))
>>
>> When we invoke the combined unit:
>>
>>  > (define-values/invoke-unit/infer factory+user@)
>>  (unit factory-user@) broke the contract
>>    (-> toy? symbol? toy?)
>>  on repaint; expected <toy?>, given: 3
>>
>> Unit Contracts
>> --------------
>>
>> However, we may not always be able to add contracts to
>> signatures.  For example, there are many already-existing
>> signatures in PLT Scheme that one may want to implement, or a
>> programmer may want to take a unit value and add contracts to it
>> after the fact.
>>
>> To do this, there is the unit/c contract combinator.  It takes a list
>> of imports and exports, where each signature is paired with a list of
>> variables and their contracts for each signature.  So if we had the
>> uncontracted version of the toy-factory^ signature:
>>
>>  (define-signature toy-factory^
>>    (build-toys repaint toy? toy-color))
>>
>> the following contracts would be appropriate for a unit that imports
>> nothing and exports that signature:
>>
>>  (unit/c (import) (export))
>>  (unit/c (import) (export toy-factory^))
>>  (unit/c
>>   (import)
>>   (export (toy-factory^
>>            [toy-color (-> toy? symbol?)])))
>>  (unit/c
>>   (import)
>>   (export (toy-factory^
>>            [build-toys (-> integer? (listof toy?))]
>>            [repaint    (-> toy? symbol? toy?)]
>>            [toy?       (-> any/c boolean?)]
>>            [toy-color  (-> toy? symbol?)])))
>>
>> Unit contracts can contain a superset of the import signatures and a
>> subset of the export signatures for a given unit value.  Also,
>> variables that are not listed for a given signature are left alone
>> when the contracts are being added.
>>
>> Since the results of applying unit/c is a new unit, then adding
>> a contract can cause link inference to fail.  For example, if we
>> change the definition of simple-factory@ above to
>>
>>  (define/contract simple-factory@
>>    (unit/c
>>     (import)
>>     (export (toy-factory^
>>              [build-toys (-> integer? (listof toy?))]
>>              [repaint    (-> toy? symbol? toy?)]
>>              [toy?       (-> any/c boolean?)]
>>              [toy-color  (-> toy? symbol?)])))
>>    (unit
>>      (import)
>>      (export toy-factory^)
>>
>>      (define-struct toy (color) #:transparent)
>>
>>      (define (build-toys n)
>>        (for/list ([i (in-range n)])
>>          (make-toy 'blue)))
>>
>>      (define (repaint t col)
>>        (make-toy col))))
>>
>> Then when we try to combine it with the factory-user@ unit, we
>> get:
>>
>>  define-compound-unit/infer: not a unit definition
>>    in: simple-factory@
>>
>> One way to solve this is to use define-unit-binding to set up the
>> static information for the new contracted value.  Another possibility
>> for unit definitions is to use define-unit/contract:
>>
>>  (define-unit/contract simple-factory@
>>    (import)
>>    (export (toy-factory^
>>             [build-toys (-> integer? (listof toy?))]
>>             [repaint    (-> toy? symbol? toy?)]
>>             [toy?       (-> any/c boolean?)]
>>             [toy-color  (-> toy? symbol?)]))
>>
>>    (define-struct toy (color) #:transparent)
>>
>>    (define (build-toys n)
>>      (for/list ([i (in-range n)])
>>        (make-toy 'blue)))
>>
>>    (define (repaint t col)
>>      (make-toy col)))
>>
>> More about these features can be found in the Reference, and a short
>> section about signature and unit contracts has been added to the Guide.
>>
>> Stevie
>> _________________________________________________
>>  For list-related administrative tasks:
>>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-dev
>



-- 
sam th
samth at ccs.neu.edu