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

From: Daniel Prager (daniel.a.prager at gmail.com)
Date: Wed Sep 4 17:33:10 EDT 2013

On Wed, Sep 4, 2013 at 7:58 AM, Matthias Felleisen <matthias at ccs.neu.edu>

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

I noticed that contract support is missing from TR.  I have, however,
constructed a roll-my-own contract example with TR, and it would be great
if Sam (or another!) pushed forward on contract support for TR.

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.

Alas, I am having trouble mentally parsing this, but may still flash it up
(with acknowledgement!) as a realistic example.

In trying to construct a simpler (yet not easily do-able with static types)
example I'm running into trouble getting my subcontract right.

I get an "n unbound identifier" error on the penultimate line:

;; make-indenter: Nat -> (String -> String)
;; Example: ((make-indenter 4) "foo") -> "    foo"
(define/contract (make-indenter n)
  (->i ([n natural-number/c])
       [r (->i ([s string?])
               [result string?]
               #:post (s result) (= (string-length result)
                                    (+ n (string-length s))))])
  (λ (s) (string-append (make-string n #\space) s)))

How should I access 'n'?

Many thanks

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20130905/37e9e432/attachment.html>

Posted on the users mailing list.