[racket-dev] A very listy Typed Racket Integer

On Jul 5, 2012 8:50 PM, "Neil Toronto" <neil.toronto at gmail.com> wrote:
>
> I just found this today:
>
>
> #lang typed/racket
>
> (define: b : (Boxof Any) (box 4))
>
> (define-predicate boxof-integer? (Boxof Integer))

This is the bug -- there's no way to write the boxof-integer? predicate,
and define- predicate shouldn't think it can.

> (define (set-b-box! v) (set-box! b v))
>
> (: a-very-listy-integer (-> Integer))
> (define (a-very-listy-integer)
>   (cond [(boxof-integer? b)  (set-b-box! '(1 2 3))
>                              (unbox b)]
>         [else  (error 'a-very-listy-integer "can't happen")]))
>
>
> > (a-very-listy-integer)
> - : Integer
> '(1 2 3)
>
>
> Is this a bug or a limitation? It can be replicated with any mutable
container type as far as I can tell.

A bug.  Anytime you get a result like that it's a bug.

>
> Also, if it's a limitation, can I get (Vectorof Index) to be a subtype of
(Vectorof Integer)?

No, that relationship would be unsound for similar reasons.

> Neil ⊥
> _________________________
>  Racket Developers list:
>  http://lists.racket-lang.org/dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/dev/archive/attachments/20120705/56a054f0/attachment.html>