[plt-scheme] Why not simpler contracts?

Henk,

try higher-order functions next, both as inputs and as outputs.

If you do come from a language with a first-order bias (say
any OOPL like Java, Eiffel, and friends, which are higher-order
but discourage you from using the language in that manner with
a biased syntax) you may think that pre/post condition specs
are the way to go.

Our biggest problem is that our combinators are repetitive.
They force people to mention things twice. Dependent contracts
are a prime example of this problem. What Robby and I have looked
at and are looking for is a macro that compiles non-repetitive
contract specs into these combinators.

So consider this a programming challenge but don't forget
my first point.

-- Matthias







On Aug 8, 2007, at 1:41 AM, Henk Boom wrote:

> Hi, I'd been using the contracts.ss library for a while. I don't mean
> any offence, but I find them almost completely unreadable =(. I know
> that obviously a lot of effort has gone into this library, but why was
> this particular syntax decided on?
>
> In any case, I've been playing around with some simple pre-post
> condition macros, and I've managed to come up with something which
> lets you specify a procedure like this:
>
> (define my-sqrt
>   (lambda/pp (x)
>     ((real? x) (>= x 0))
>     (result
>      (or (and (< x 1) (> result x))
>          (and (> x 1) (< result x))))
>     (sqrt x)))
>
>> (my-sqrt 'a)
> precondition failed:  (real? x)
>
>  === context ===
> stdin::19: my-sqrt
>
>> (my-sqrt -1)
> precondition failed:  (>= x 0)
>
>  === context ===
> stdin::19: my-sqrt
>
>> (my-sqrt 9)
> 3
>> (my-sqrt 0.25)
> 0.5
>> (my-sqrt 1)
> postcondition failed:  (or (and (< x 1) (> result x)) (and (> x 1) (<
> result x)))
>
>  === context ===
> stdin::19: my-sqrt
>
> (The error messages are more helpful with errortrace =)
>
> I like this because I find it to be a very clear and simple syntax,
> though I admit it falls short in a couple of areas (returning multiple
> values for one). Does anyone have any comments?
>
> In case you're interested, here's the code. Don't be too tough on it,
> though improvements are welcome. I'm still a macro noob =).
>
> (module private-pp mzscheme
>
>   (provide lambda/pp-full)
>   (define-syntax lambda/pp-full
>     (syntax-rules ()
>       ((lambda/pp-full args preconditions () . body)
>         (lambda args
>           (do-conditions "precondition" . preconditions)
>           (begin . body)))
>       ((lambda/pp-full args preconditions (result .  
> postconditions) . body)
>         (lambda args
>           (do-conditions "precondition" . preconditions)
>           (let ((result (begin . body)))
>             (do-conditions "postcondition" . postconditions)
>             result)))))
>
>   (provide lambda/pp-pre-only)
>   (define-syntax lambda/pp-pre-only
>     (syntax-rules ()
>       ((lambda/pp-pre-only args preconditions post-stuff . body)
>         (lambda/pp-full args preconditions () . body))))
>
>   (provide lambda/pp-none)
>   (define-syntax lambda/pp-none
>     (syntax-rules ()
>       ((lambda/pp-none args preconditions post-stuff . body)
>         (lambda/pp-full args () () . body))))
>
>   (define-syntax do-conditions
>     (syntax-rules ()
>       ((do-contitions str)
>         ())
>       ((do-conditions str ())
>         ())
>       ((do-conditions str cond1)
>         (if (not cond1)
>           (error (format "~a failed: " str) 'cond1)
>           #t))
>       ((do-conditions str cond1 . conds)
>         (begin (do-conditions str cond1)
>                (do-conditions str . conds)))))
>
>   ) ;; end module
>
> (module pp-full mzscheme
>   (require "private-pp.ss")
>
>   (provide (rename lambda/pp-full lambda/pp))
>
>   ) ;; end module
>
> (I also have pp-pre-only and pp-none modules, useful for speed or to
> preserve tail recursion)
>
>     Henk Boom
> _________________________________________________
>   For list-related administrative tasks:
>   http://list.cs.brown.edu/mailman/listinfo/plt-scheme