{"size": 2635, "ext": "scrbl", "max_stars_repo_path": "pkgs/racket-doc/scribblings/guide/contracts/exists.scrbl", "max_stars_repo_name": "lkh01/racket", "max_stars_repo_stars_event_min_datetime": "2018-07-29T04:13:52.000Z", "max_stars_repo_stars_event_max_datetime": "2022-02-14T16:11:17.000Z", "max_issues_repo_path": "pkgs/racket-doc/scribblings/guide/contracts/exists.scrbl", "max_issues_repo_name": "lkh01/racket", "max_issues_repo_issues_event_min_datetime": "2017-08-25T20:26:37.000Z", "max_issues_repo_issues_event_max_datetime": "2022-02-26T17:48:40.000Z", "max_forks_repo_path": "pkgs/racket-doc/scribblings/guide/contracts/exists.scrbl", "max_forks_repo_name": "lkh01/racket", "max_forks_repo_forks_event_min_datetime": "2016-04-25T11:47:57.000Z", "max_forks_repo_forks_event_max_datetime": "2017-05-09T14:52:48.000Z"}
{"max_stars_count": 10, "max_issues_count": 15, "max_forks_count": 3, "avg_line_length": 43.9166666667, "max_line_length": 93, "alphanum_fraction": 0.669829222}
#lang scribble/doc
@(require scribble/manual scribble/eval "utils.rkt"
          (for-label racket/contract))

@title[#:tag "contracts-exists"]{Abstract Contracts using @racket[#:exists] and @racket[#:∃]}

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 Queue Example}

@margin-note{
  You can type @racket[#:exists] instead of @racket[#:∃] if you 
cannot easily type unicode characters; in DrRacket, typing
@litchar{\exists} followed by either alt-\ or control-\ (depending
on your platform) will produce @racket[∃].}
The @racket[contract-out] form allows you to write
@racketblock[#:∃ _name-of-a-new-contract] as one of its clauses. This declaration
introduces the variable @racket[_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 queue data structure:
@racketmod[racket
           (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-out
             [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 @racket[car] and @racket[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 queue representation is abstract, we can use @racket[#:∃] in the
@racket[contract-out] expression, like this:
@racketblock[(provide
              (contract-out
               #:∃ queue
               [empty queue]
               [enq (-> integer? queue queue)]
               [next (-> queue integer?)]
               [deq (-> queue queue)]
               [empty? (-> queue boolean?)]))]

Now, if clients of the data structure try to use @racket[car] and @racket[cdr], they
receive an error, rather than mucking about with the internals of the queues.

See also @ctc-link["exists-gotcha"].
