[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 18:59:30 EDT 2013

Thanks Robby

... and I was so close!

The revised and improved version of the slides is up:

http://www.slideshare.net/DanielPrager/introduction-to-contracts-and-functional-contracts


Cheers

Dan



On Thu, Sep 5, 2013 at 7:37 AM, Robby Findler
<robby at eecs.northwestern.edu>wrote:

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


-- 
*Daniel Prager*
Agile/Lean Coaching, Software Development and Leadership
Twitter: @agilejitsu <https://twitter.com/agilejitsu>
Blog: agile-jitsu.blogspot.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20130905/19743f5d/attachment.html>

Posted on the users mailing list.