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

From: Jay McCarthy (jay.mccarthy at gmail.com)
Date: Mon Jun 2 02:06:14 EDT 2014

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


Posted on the dev mailing list.