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

I agree, but do you think that `lambda' should provide a better error
message for all the cases here, or that `with-contract' should handle
this case specially?  Or are you just objecting to the semi-expanded
code in the output there?

sam th

On Sun, Feb 15, 2009 at 6:51 PM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:
>
> 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
>
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-dev
>



-- 
sam th
samth at ccs.neu.edu