[racket-dev] [plt] Push #28829: master branch updated

On Jun 2, 2014, at 2:06 AM, Jay McCarthy wrote:

> Your research suggests that contracts are the only meaningful higher-order assertions, so this thing is assert/higher-order and the contract DSL is the right way to specify the condition.


I am not sure I would go this far. Suppose you want to insert these 'assert' expressions for the sake of logical verification rather than actual checking. I just don't know whether our work is helpful. See Christos's TOPLAS paper. 

;; --- 

I think the separation of assert from assert/ho is useful from a performance perspective. The former is cheap, the latter imposes a non-trivial, distributed cost. In contrast to contracts, assert/ho avoids the cost of blame calculations. All we need to know when it blows up is which assertion turned out to be wrong. While I am not sure how much cheaper it is to run assertions compared to contract, my hunch is that it is cheaper and that we should keep the option open to opt for this cheaper version. 

-- Matthias










On Jun 2, 2014, at 2:06 AM, Jay McCarthy wrote:

> Ok. I thought about what kinds of things might be different in the
> future with more understanding and experience using assertions...
> 
> How about this: Start an assert library with two exports,
> assert/higher-order and assert. Your research suggests that contracts
> are the only meaningful higher-order assertions, so this thing is
> assert/higher-order and the contract DSL is the right way to specify
> the condition. On the other hand, assert would be like the traditional
> one that using expressions. Another name for a/ho would be
> assert/contract which might be useful for using contracts for flat
> values. (The name though, only communicates mechanism and not the
> purpose like h-o.)
> 
> Jay
> 
> On Sun, Jun 1, 2014 at 6:14 PM, Robby Findler
> <robby at eecs.northwestern.edu> wrote:
>> (I must have missed that suggestion, sorry.)
>> 
>> I don't object to the sentiment behind the name, but I feel like we
>> have not figured out the best way to do assertions or invariants and
>> so we should leave such a valuable name for a future
>> contributor/insight and use the more "ugly" name for this one.
>> 
>> Even if that name ends up in a different library, I wouldn't want an
>> assertion/invariant library to conflict with racket/contract.
>> 
>> Robby
>> 
>> 
>> On Sun, Jun 1, 2014 at 6:57 PM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>>> 
>>> I suggested exactly that name in a private message to Robby.
>>> 
>>> 
>>> 
>>> On Jun 1, 2014, at 7:49 PM, Jay McCarthy wrote:
>>> 
>>>> Based on this commit, I feel like "assert" would be a better name than
>>>> "invariant-assertion". I can imagine putting these on various internal
>>>> parts of a function where the self-blame would be justified. The
>>>> (define id (assert ctc e)) pattern is just one common use.
>>>> 
>>>> Jay
>>>> 
>>>> On Sat, May 31, 2014 at 1:46 PM,  <matthias at racket-lang.org> wrote:
>>>>> matthias has updated `master' from 9d94ef725e to 89dea63995.
>>>>> http://git.racket-lang.org/plt/9d94ef725e..89dea63995
>>>>> 
>>>>> =====[ One Commit ]=====================================================
>>>>> Directory summary:
>>>>> 84.2% pkgs/racket-pkgs/racket-doc/scribblings/reference/
>>>>> 11.0% racket/collects/racket/contract/private/
>>>>>  4.6% racket/collects/racket/contract/
>>>>> 
>>>>> ~~~~~~~~~~
>>>>> 
>>>>> 89dea63 Matthias Felleisen <matthias at racket-lang.org> 2014-05-31 15:45
>>>>> :
>>>>> | removed _contract_ language from _invariant-..._ as much as possible
>>>>> |
>>>>> | added a hint as to why the error message uses the inappropriate contract language
>>>>> :
>>>>> M racket/collects/racket/contract/private/base.rkt  |  4 ++--
>>>>> M racket/collects/racket/contract/region.rkt        |  2 +-
>>>>> M .../scribblings/reference/contracts.scrbl         | 22 ++++++++++----------
>>>>> 
>>>>> =====[ Overall Diff ]===================================================
>>>>> 
>>>>> pkgs/racket-pkgs/racket-doc/scribblings/reference/contracts.scrbl
>>>>> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>>>>> --- OLD/pkgs/racket-pkgs/racket-doc/scribblings/reference/contracts.scrbl
>>>>> +++ NEW/pkgs/racket-pkgs/racket-doc/scribblings/reference/contracts.scrbl
>>>>> @@ -1509,24 +1509,24 @@ The @racket[define-struct/contract] form only allows a subset of the
>>>>> (make-salmon #f 'pacific)
>>>>> ]}
>>>>> 
>>>>> - at defform[(invariant-contract contract-expr expr)]{
>>>>> -  Establishes an invariant of @racket[expr], determined by @racket[contract-expr].
>>>>> + at defform[(invariant-assertion invariant-expr expr)]{
>>>>> +  Establishes an invariant of @racket[expr], determined by @racket[invariant-expr].
>>>>> 
>>>>> -  Unlike other ways to attach contracts to values, an
>>>>> -  @racket[invariant-contract] does not establish a boundary
>>>>> -  between two parties. Instead, it simply puts the contract
>>>>> -  on the value, treating the module containing the
>>>>> -  @racket[invariant-contract] expression as the party to be blamed
>>>>> -  for any violations of the contract.
>>>>> +  Unlike the specification of a contract, an
>>>>> +  @racket[invariant-assertion] does not establish a boundary
>>>>> +  between two parties. Instead, it simply attaches a logical assertion
>>>>> +  to the value. Because the form uses contract machinery to check the
>>>>> +  assertion, the surround module is treated as the party to be blamed
>>>>> +  for any violations of the assertion.
>>>>> 
>>>>> -  This means, for example, that the contract is checked on
>>>>> +  This means, for example, that the assertion is checked on
>>>>>  recursive calls, when an invariant is used on the right-hand
>>>>> -  side of a definition.
>>>>> +  side of a definition:
>>>>> 
>>>>>  @examples[#:eval
>>>>>            furlongs->feet-eval
>>>>>            (define furlongss->feets
>>>>> -              (invariant-contract
>>>>> +              (invariant-assertion
>>>>>               (-> (listof real?) (listof real?))
>>>>>               (λ (l)
>>>>>                 (cond
>>>>> 
>>>>> racket/collects/racket/contract/private/base.rkt
>>>>> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>>>>> --- OLD/racket/collects/racket/contract/private/base.rkt
>>>>> +++ NEW/racket/collects/racket/contract/private/base.rkt
>>>>> @@ -3,7 +3,7 @@
>>>>> (provide contract
>>>>>         (rename-out [-recursive-contract recursive-contract])
>>>>>         current-contract-region
>>>>> -         invariant-contract)
>>>>> +         invariant-assertion)
>>>>> 
>>>>> (require (for-syntax racket/base syntax/name syntax/srcloc)
>>>>>         racket/stxparam
>>>>> @@ -89,7 +89,7 @@
>>>>>          (procedure-rename new-val vs-name)])]
>>>>>      [else new-val])))
>>>>> 
>>>>> -(define-syntax (invariant-contract stx)
>>>>> +(define-syntax (invariant-assertion stx)
>>>>>  (syntax-case stx ()
>>>>>    [(_ ctc e)
>>>>>     (quasisyntax/loc stx
>>>>> 
>>>>> racket/collects/racket/contract/region.rkt
>>>>> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
>>>>> --- OLD/racket/collects/racket/contract/region.rkt
>>>>> +++ NEW/racket/collects/racket/contract/region.rkt
>>>>> @@ -4,7 +4,7 @@
>>>>>         define/contract
>>>>>         with-contract
>>>>>         current-contract-region
>>>>> -         invariant-contract)
>>>>> +         invariant-assertion)
>>>>> 
>>>>> (require (for-syntax racket/base
>>>>>                     racket/struct-info
>>>> 
>>>> 
>>>> 
>>>> --
>>>> Jay McCarthy <jay at cs.byu.edu>
>>>> Assistant Professor / Brigham Young University
>>>> http://faculty.cs.byu.edu/~jay
>>>> 
>>>> "The glory of God is Intelligence" - D&C 93
>>> 
>>> 
>>> _________________________
>>>  Racket Developers list:
>>>  http://lists.racket-lang.org/dev
> 
> 
> 
> -- 
> Jay McCarthy <jay at cs.byu.edu>
> Assistant Professor / Brigham Young University
> http://faculty.cs.byu.edu/~jay
> 
> "The glory of God is Intelligence" - D&C 93