[plt-scheme] macro question

If you want to use contracts in Typed Scheme, do you have to restate
all the aspects of the contract that are already checked by the type
system, or can you just focus on the properties that are not enforced
by the type system (e.g. input must be a *positive* integer)?

--Mark

On Tue, Jun 10, 2008 at 2:41 PM, Matthias Felleisen
<matthias at ccs.neu.edu> wrote:

> Before we talk too abstractly here, let's look at an example:
>
> UNTYPED
>
>> #lang scheme
>>
>> ;; An A is one of:
>> ;; -- Number
>> ;; -- Boolean
>> ;; -- (cons A A)
>>
>> ;; A -> Number
>> ;; compute the sum of all numbers in the tree
>> (define (Sigma tree)
>>  (cond
>>    [(number? tree) tree]
>>    [(boolean? tree) 0]
>>    [else (+ (Sigma (car tree)) (Sigma (cdr tree)))]))
>>
>> (= (Sigma (cons (cons #t 5) 0)) 5)
>
> TYPED:
>
>> #lang typed-scheme
>>
>> (define-type-alias A (mu A (U Number Boolean (cons A A))))
>>
>> (: Sigma (A -> Number))
>> ;; compute the sum of all numbers in the tree
>> (define (Sigma tree)
>>  (cond
>>    [(number? tree) tree]
>>    [(boolean? tree) 0]
>>    [else (+ (Sigma (car tree)) (Sigma (cdr tree)))]))
>>
>> (= (Sigma (cons (cons #t 5) 0)) 5)
>>
>
>
> In general, Typed Scheme is as compact as untyped Scheme in HtDP style. And
> it is checked for you. -- Matthias
>