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

From: Matthias Felleisen (matthias at ccs.neu.edu)
Date: Sun Feb 15 18:51:45 EST 2009

I am sorry, but

> Welcome to DrScheme, version 4.1.4.3-svn13feb2009 [3m].
> Language: Module; memory limit: 128 megabytes.
> . begin (possibly implicit): no expression after a sequence of  
> internal definitions in: ((define-syntax current-contract-region11  
> (convert-renamer (λ (stx) (syntax (quote (region f1)))))) (expand- 
> ssp-body (current-contract-region1) (current-contract-region11)  
> (with-contract-helper #<procedure:syntax-introducer> (quote (region  
> f1)) ((g number?)) () (define g 10))))
> >

is indefensible.


On Feb 15, 2009, at 2:57 PM, Sam TH wrote:

> 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



Posted on the dev mailing list.