[racket] help with typed racket function?

On Sun, Mar 13, 2011 at 8:36 PM, Danny Yoo <dyoo at cs.wpi.edu> wrote:
> I'm trying to make a function that can discriminate typed boxes: I
> tried the following in Typed Racket:
>
> (: ensure-number-box (Any -> (Boxof Number)))
> (define (ensure-number-box x)
>  (if (and (box? x) (number? (unbox x)))
>      x
>      (error 'ensure-number-box "~s" x)))
>
> Unfortunately, I can't convince the type checker that x is a (Boxof
> number).  I'm not quite sure how to use the occurrence typing properly
> to get this to type correctly.

As Eli says, you can't do this.  Here's another way of showing why:

(define: any-box : (Boxof Any) (box #{3 :: Any})) ;; safe, the
contents is an Any
(define: num-box : (Boxof Number) (ensure-number-box any-box)) ;;
typechecks, given the return type you wanted
(set-box! any-box #f) ;; ok, since any-box is a box of anything
(unbox num-box) ;; Type: Number, Value: #f -- oh no!

-- 
sam th
samth at ccs.neu.edu