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

From: Robby Findler (robby at eecs.northwestern.edu)
Date: Wed Sep 4 17:37:09 EDT 2013

You need to indicate that the contract on 'r' needs 'n', ie replace "[r
(->i"  with "[r (n) (->i".

Robby


On Wed, Sep 4, 2013 at 4:33 PM, Daniel Prager <daniel.a.prager at gmail.com>wrote:

> On Wed, Sep 4, 2013 at 7:58 AM, Matthias Felleisen <matthias at ccs.neu.edu>
>  wrote:
>
> 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
>
> Dan
>
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20130904/630811d2/attachment-0001.html>

Posted on the users mailing list.