[plt-dev] abstract contracts

On Sun, Sep 6, 2009 at 3:14 PM, Robby
Findler<robby at eecs.northwestern.edu> wrote:
> Right. That wouldn't be parametric.

I think it's the contracts-don't-change-programs condition, not the
parametricity condition, that would be violated here.

-jacob


>
> Robby
>
> On Sat, Sep 5, 2009 at 7:58 PM, Matthias Felleisen<matthias at ccs.neu.edu> wrote:
>>
>> On Sep 5, 2009, at 6:04 PM, Robby Findler wrote:
>>
>>> No. As we discussed, there can't be with this meaning of #:exists. If
>>> there were, you'd run into the same problem as with number? (for those
>>> that don't know what I'm talking about, see the new second gotcha
>>> section in the contracts documentation in the guide).
>>>
>>> But, if you want to protect yourself by shifting blame, you can still
>>> do that. You need to use the 'stack' contract in your own code to do
>>> so instead of using a predicate test.
>>
>> So the client can write additional contracts involving stacks, e.g.,
>>
>>  [stack-append (-> stack stack stack)]
>>
>> but it is impossible to write data definitions such as
>>
>>  A collection is one of:
>>   -- stack
>>   -- queue
>>
>> and then use it because you can't distinguish a stack from a queue. (Of
>> course, if both stacks and queues support the same operations, you can do
>> this.)
>>
>> -- Matthias
>>
>>
>>
>>
>>> Robby
>>>
>>> On Sat, Sep 5, 2009 at 10:02 AM, Matthias Felleisen<matthias at ccs.neu.edu>
>>> wrote:
>>>>
>>>> Is there a stack? predicate afterwards?
>>>>
>>>> On Sep 4, 2009, at 2:00 PM, Robby Findler wrote:
>>>>
>>>>> I've added #:exists to provide/contract, as a way to hide information
>>>>> ala "type t" declarations on ML signatures.
>>>>>
>>>>> See the contracts section in the Guide for a worked example and a
>>>>> discussion of a gotcha. The short version is that you can now write
>>>>> things like this:
>>>>>
>>>>> (provide/contract
>>>>>  #:exists stack
>>>>>  [new stack]
>>>>>  [push (-> int stack stack)]
>>>>>  [pop (-> (and/c stack non-empty?) int)]
>>>>>  [non-empty? (-> stack boolean?)])
>>>>>
>>>>> and have the contract system enforce data abstraction, even if your
>>>>> stack operations are simply these:
>>>>>
>>>>>  (define new '())
>>>>>  (define push cons)
>>>>>  (define pop car)
>>>>>  (define non-empty? pair?)
>>>>>
>>>>> That is, clients of your module will not be able to treat your stacks
>>>>> as if they were lists, even though they really are lists.
>>>>>
>>>>> Robby
>>>>> _________________________________________________
>>>>>  For list-related administrative tasks:
>>>>>  http://list.cs.brown.edu/mailman/listinfo/plt-dev
>>>>
>>>>
>>
>>
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-dev
>
>