[plt-dev] abstract contracts

From: Robby Findler (robby at eecs.northwestern.edu)
Date: Sun Sep 6 18:14:32 EDT 2009

Right. That wouldn't be parametric.

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
>>>
>>>
>
>


Posted on the dev mailing list.