[racket] typed racket error

On Sun, Apr 20, 2014 at 10:39 AM, Alexander D. Knauth
<alexander at knauth.org> wrote:
> I’m trying to make a multiplication function that can take either all
> numbers or all numbers and one vector, and have it not matter what order
> they come in.  To do this, I’m using match with list-no-order:
> #lang typed/racket
>
> (require plot/typed/utils)
>
> (define listof-number?
>   (make-predicate (Listof Number)))
>
> (: my* (case->
>         (-> One)
>         (Number Number * -> Number)
>         ((Vectorof Real) Real * -> (Vectorof Real))
>         (Real (Vectorof Real) Real * -> (Vectorof Real))
>         (Real Real (Vectorof Real) Real * -> (Vectorof Real))
>         (Real Real Real (Vectorof Real) Real * -> (Vectorof Real))
>         (Real Real Real Real (Vectorof Real) Real * -> (Vectorof Real))))
>         ; if I could, I would do this:
>         ; (Real * (Vectorof Real) Real * -> (Vectorof Real))
>
> (define my*
>   (case-lambda
>     [() 1]
>     [args (match args
>             [(list-no-order (? vector? v) (? real? ns) ...)
>              (v* v (apply * ns))]
>             [(? listof-number? ns)
>              (apply * ns)])]))
>
> It’s giving me these errors:
> . Type Checker: Expected One, but got Number in: (apply * ns) ; why is it
> expecting One there?
This looks like a bug.
> . Type Checker: Expected (Vectorof Real), but got Any in: v ; the type
> shouldn’t be Any, it should at least
>                                                             ; be VectorTop,
> and with the type annotation
>                                                             ; for my* should
> tell it that all of the
>                                                             ; vectors are
> (Vectorof Real), right?
That is assuming a simple expansion in match (that TR can follow)
which isn't a valid assumption.
> . Type Checker: Bad arguments to function in apply: ; shouldn’t it be able
> to tell that ns is a
> Domains: Number *                                   ; (Listof Number),
> especially since
> Arguments: (Listof Any) *                           ; listof-number? was
> defined with
>  in: (apply * ns)                                   ; make-predicate?
> . Type Checker: Expected One, but got (Vectorof Real) in: (v* v (apply *
> ns)) ; why is it expecting One?
Same bug as above.
> . Type Checker: Expected Number, but got (Vectorof Real) in: (v* v (apply *
> ns)) ;why is it expecting Number?
Because it is typechecking the case where there are no vectors and
doesn't know that this branch is dead code.
> . Type Checker: Expected (Vectorof Real), but got Number in: (apply *
> ns);whyis it expecting (Vectorof Real)?
Reverse of the above.
>
>
>
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users
>