61 lines
2.6 KiB
Racket
61 lines
2.6 KiB
Racket
#lang scribble/doc
|
|
@(require scribble/manual
|
|
scribble/eval
|
|
"guide-utils.ss"
|
|
"contracts-utils.ss"
|
|
(for-label scheme/contract))
|
|
|
|
@title[#:tag "contracts-exists"]{Abstract Contracts using @scheme[#:exists] and @scheme[#:∃]}
|
|
|
|
The contract system provides existential contracts that can
|
|
protect abstractions, ensuring that clients of your module
|
|
cannot depend on the precise representation choices you make
|
|
for your data structures.
|
|
|
|
@ctc-section{Getting Started, with a Stack Example}
|
|
|
|
@margin-note{
|
|
You can type @scheme[#:exists] instead of @scheme[#:∃] if you
|
|
cannot easily type unicode characters; in DrScheme, typing
|
|
@tt{\exists} followed by either alt-\ or control-\ (depending
|
|
on your platform) will produce @scheme[∃].}
|
|
The @scheme[provide/contract] form allows you to write
|
|
@schemeblock[#:∃ _name-of-a-new-contract] as one of its clauses. This declaration
|
|
introduces the variable @scheme[_name-of-a-new-contract], binding it to a new
|
|
contract that hides information about the values it protects.
|
|
|
|
As an example, consider this (simple) implementation of a stack datastructure:
|
|
@schememod[scheme
|
|
(define empty '())
|
|
(define (enq top queue) (append queue (list top)))
|
|
(define (next queue) (car queue))
|
|
(define (deq queue) (cdr queue))
|
|
(define (empty? queue) (null? queue))
|
|
|
|
(provide/contract
|
|
[empty (listof integer?)]
|
|
[enq (-> integer? (listof integer?) (listof integer?))]
|
|
[next (-> (listof integer?) integer?)]
|
|
[deq (-> (listof integer?) (listof integer?))]
|
|
[empty? (-> (listof integer?) boolean?)])]
|
|
This code implements a queue purely in terms of lists, meaning that clients
|
|
of this data structure might use @scheme[car] and @scheme[cdr] directly on the
|
|
data structure (perhaps accidentally) and thus any change in the representation
|
|
(say to a more efficient representation that supports amortized constant time
|
|
enqueue and dequeue operations) might break client code.
|
|
|
|
To ensure that the stack representation is abstact, we can use @scheme[#:∃] in the
|
|
@scheme[provide/contract] expression, like this:
|
|
@schemeblock[(provide/contract
|
|
#:∃ stack
|
|
[empty stack]
|
|
[enq (-> integer? stack stack)]
|
|
[next (-> stack integer?)]
|
|
[deq (-> stack (listof integer?))]
|
|
[empty? (-> stack boolean?)])]
|
|
|
|
Now, if clients of the data structure try to use @scheme[car] and @scheme[cdr], they
|
|
receive an error, rather than mucking about with the internals of the queues.
|
|
|
|
See also @ctc-link["exists-gotcha"].
|