[racket] Introductory talk on Contracts and Functional Contracts, with most examples in Racket

On Sep 3, 2013, at 5:51 PM, Daniel Prager <daniel.a.prager at gmail.com> wrote:

> Hi Matthias
> 
> Thank-you for your sage advice:
> 
> On Tue, Sep 3, 2013 at 11:54 PM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
> 
> 1. Always use contracts that cannot be expressed as types
> in an obvious type system.
> 
> I'll work on my examples.  I may also throw in an example in typed racket to show the types and contracts working together.


You can't. Sam has had this combination on his todo list for 7 years and he never got around to it. Perhaps I signed his dissertation too early :-)



> 2. Show a higher-order contract and flavors that push this idea hard. Consider using d/dx or indefinite adaptive integral ...

> I'm a little bit wary of showing (only) a calculus-flavoured example because I don't want to give the impression that  the higher-order contracts are just for mathematical applications.


Good. So use this: 

 (contract-out 
  ;; Nat Nat [Nat] [Nat] [[Listof X]] [[Listof Y]] ->* Image [Nat Nat ->* X Y]
  ;; (grid n m x-delta y-delta x-labels y-labels) creates:
  ;; -- a graphical grid of size (* n x-delta) x (* m y-delta) 
  ;;    divvied up into n x m tiles of size x-delta x y-delta 
  ;;    labeled with x-labels x y-labels 
  ;; -- a function event-handler that deals with mouse clicks for this grid 
  ;; (event-handler x y) = (an-x-lablel, a-y-label)
  ;; iff (x,y) is a mouse click in the tile labeled (an-x-lablel, a-y-label) 
  (grid (->i ((n natural-number/c) (m natural-number/c))
             ((delta-x natural-number/c) 
              (delta-y natural-number/c) 
              (x-labels list?)
              (y-labels list?)
              #:grid? (grid? #t))
             #:pre/name (n x-labels) "correct # of x labels"
             (or (unsupplied-arg? x-labels) (= (length x-labels) n))
             #:pre/name (m y-labels) "correct # of y labels"
             (or (unsupplied-arg? y-labels) (= (length y-labels) m))
             (values
              (grid-scene image?)
              (event-handler 
               (delta-x delta-y n m x-labels y-labels)
               (->i ((x natural-number/c) (y natural-number/c))
                    #:pre/name (x) "x in proper range"
                    (or (unsupplied-arg? delta-x) (< x (* n delta-x)))
                    #:pre/name (y) "y in proper range"
                    (or (unsupplied-arg? delta-y) (< y (* m delta-y)))
                    (values (xl (if (unsupplied-arg? x-labels) any/c (apply or/c x-labels)))
                            (yl (if (unsupplied-arg? y-labels) any/c (apply or/c y-labels)))))))))

This is from my code base. It is a function that consumes the dimensions of a (functional image) canvas and created a gridded image and an event handler that tells you on which "tile" a user clicked. It is highly real, higher-order, dependent, and yet not difficult to understand. 

Full code below. 


> I confess that as I have been learning about higher-order contracts I wondered whether (instead) types + flat-contracts would suffice in practice as a worse-is-better compromise.

That's what Meyer thought with Eiffel. It assumes a closed world of software project with a central registry of higher-order types combined with contracts to avoid rampant code duplication. Some people want to live in this world; real people can't. 


> 3. For the smack-down, contracts tend to reveal some things that are "intensional" (part of the implementation).
> 
> Sounds bad for information hiding.  What's an example of this?

The error estimate for adaptive integration is a function of the delta you impose on one "iteration" of the algorithm. 

-- Matthias


;; ---------------------------------------------------------------------------------------------------
(provide
 (contract-out 
  ;; Nat Nat [Nat] [Nat] [[Listof X]] [[Listof Y]] ->* Image [Nat Nat ->* X Y]
  ;; (grid n m x-delta y-delta x-labels y-labels) creates:
  ;; -- a graphical grid of size (* n x-delta) x (* m y-delta) 
  ;;    divvied up into n x m tiles of size x-delta x y-delta 
  ;;    labeled with x-labels x y-labels 
  ;; -- a function event-handler that deals with mouse clicks for this grid 
  ;; (event-handler x y) = (an-x-lablel, a-y-label)
  ;; iff (x,y) is a mouse click in the tile labeled (an-x-lablel, a-y-label) 
  (grid (->i ((n natural-number/c) (m natural-number/c))
             ((delta-x natural-number/c) 
              (delta-y natural-number/c) 
              (x-labels list?)
              (y-labels list?)
              #:grid? (grid? #t))
             #:pre/name (n x-labels) "correct # of x labels"
             (or (unsupplied-arg? x-labels) (= (length x-labels) n))
             #:pre/name (m y-labels) "correct # of y labels"
             (or (unsupplied-arg? y-labels) (= (length y-labels) m))
             (values
              (grid-scene image?)
              (event-handler 
               (delta-x delta-y n m x-labels y-labels)
               (->i ((x natural-number/c) (y natural-number/c))
                    #:pre/name (x) "x in proper range"
                    (or (unsupplied-arg? delta-x) (< x (* n delta-x)))
                    #:pre/name (y) "y in proper range"
                    (or (unsupplied-arg? delta-y) (< y (* m delta-y)))
                    (values (xl (if (unsupplied-arg? x-labels) any/c (apply or/c x-labels)))
                            (yl (if (unsupplied-arg? y-labels) any/c (apply or/c y-labels)))))))))))

;; ---------------------------------------------------------------------------------------------------
;; implementation section 

(require 2htdp/image)
(module+ test 
  (require rackunit))

(define/contract 
  (grid n m (delta-x 20) (delta-y 20) (x-labels (build-list n add1)) (y-labels (build-list m add1))
        #:grid? (grid? #t))
  #;
  (->i ((n natural-number/c) (m natural-number/c))
       ((delta-x natural-number/c) 
        (delta-y natural-number/c) 
        (x-labels list?)
        (y-labels list?)
        #:grid? (grid? #t))
       #:pre/name (n x-labels) "correct # of x labels"
       (or (unsupplied-arg? x-labels) (= (length x-labels) n))
       #:pre/name (m y-labels) "correct # of y labels"
       (or (unsupplied-arg? y-labels) (= (length y-labels) m))
       (values
        (grid-scene image?)
        (event-handler 
         (delta-x delta-y n m x-labels y-labels)
         (->i ((x natural-number/c) (y natural-number/c))
              #:pre/name (x) "x in proper range"
              (or (unsupplied-arg? delta-x) (< x (* n delta-x)))
              #:pre/name (y) "y in proper range"
              (or (unsupplied-arg? delta-y) (< y (* m delta-y)))
              (values (xl (if (unsupplied-arg? x-labels) any/c (apply or/c x-labels)))
                      (yl (if (unsupplied-arg? y-labels) any/c (apply or/c y-labels))))))))
  any/c
  (values (image-grid n m delta-x delta-y grid?)
          (lambda (x y) 
            (values (search x x-labels delta-x) (search y y-labels delta-y)))))

;; Nat Nat Nat Nat Boolean -> Image 
(define (image-grid n m delta-x delta-y grid?)
  (define tile (rectangle delta-x delta-y 'outline (if grid? 'black 'white)))
  (define arow (apply beside (make-list n tile)))
  (define col* (apply above  (make-list m arow)))
  col*)

;; Nat [Listof X] Nat -> X 
(module+ test
  (check-equal? (search 95 (build-list 20 add1) 10) 10))
(define/contract (search z labels delta)
  (->i ((z natural-number/c) (labels (listof any/c)) (delta natural-number/c))
       #:pre (z labels delta) (< z (* (length labels) delta))
       any)
  (cond
    [(< z delta) (first labels)]
    [else (search (- z delta) (rest labels) delta)]))

(module+ test 
  (define n 20)
  (define m 20)
  (define x-labels (build-list n add1))
  (define y-labels (build-list m add1))
  (check-equal? (let*-values (((_ g) (grid n m 10 10 x-labels y-labels))
                              ((x y) (g 99 99)))
                  (cons x y))
                (cons 10 10))
  (check-equal? (let*-values (((_ g) (grid 20 20 10 10)) 
                              ((x y) (g 99 99)))
                  (cons x y))
                (cons 10 10))
  (check-equal? (let*-values (((_ g) (grid 20 20)) 
                              ((x y) (g 99 99)))
                  (cons x y))
                (cons 5 5)))

;; ---------------------------------------------------------------------------------------------------
;; for exploration only
(require 2htdp/universe)
(define (play)
  (define-values (background keyhandler) (grid 20 20 50 50 #:grid? #f))
  (define (add-dot p i)
    (match p
      [`(,x ,a ,y ,b)
       (define label (text (format "(~a,~a)" a b) 22 'black))
       (place-image/align label x y "center" "center" i)]))
  (big-bang '()
            (to-draw (λ (w) (foldr add-dot background w)))
            (on-mouse (λ (w x y me)
                        (cond
                          [(mouse=? "button-down" me)
                           (define-values (a b) (keyhandler x y))
                           (cons (list x a y b) w)]
                          [else w])))))