[racket] 3D Plot example doesn't work in Typed Racket

This is one case in which Typed Racket could do better inference. I'm 
not sure what the difference is between Listof and Sequenceof that makes 
it treat them differently, but it does:

#lang typed/racket

;; Typechecks
(ann (list (vector 1 2 3))
      (Listof (Vector Any Any (U Real False))))

;; Fails
(ann (list (vector 1 2 3))
      (Sequenceof (Vector Any Any (U Real False))))

;; Typechecks
(ann (list (ann (vector 1 2 3)
                 (Vector Any Any (U Real False))))
      (Sequenceof (Vector Any Any (U Real False))))


If there shouldn't be a difference, it's an error that needs a bug report.

In the meantime, use lists. This works fine:

#lang typed/racket   ;<- typed
(require plot/typed) ;<- typed
(plot-new-window? #t)
(plot3d (discrete-histogram3d '((a a 1) (a b 2) (b b 3))
                               #:label "Missing (b,a)"
                               #:color 4 #:line-color 4))


Neil ⊥

On 05/30/2014 01:50 PM, Alexander D. Knauth wrote:
> The problem isn’t with List vs. Sequenceof, the problem is that (Vector
> Symbol Symbol Integer) isn’t a subtype of (Vector Any Any (U Real False
> ivl)).
> #lang typed/racket
> (require plot/typed)
> (ann (cast 0 (Vector Symbol Symbol Integer)) (Vector Any Any (U Real
> False ivl)))
>
> Also (Vector Symbol) isn’t a subtype of (Vector Any), either.
>
> You can solve this problem by doing this:
> #lang typed/racket   ;<- typed
> (require plot/typed) ;<- typed
> (plot-new-window? #t)
> (plot3d (discrete-histogram3d (ann '(#(a a 1) #(a b 2) #(b b 3))
>                                     (List (Vector Any Any (U Real False
> ivl))
>                                           (Vector Any Any (U Real False
> ivl))
>                                           (Vector Any Any (U Real False
> ivl))))
>                                #:label "Missing (b,a)"
>                                #:color 4 #:line-color 4))
>
> The type (Vector Symbol Symbol Integer) can’t be a subtype of (Vector
> Any Any (U Real False ivl)) because Vectors are mutable.
>  From the perspective of an accessor it should be a subtype, but from
> the perspective of a mutator it should be the other way around.
>
> At one point I submitted a bug report about this, but it turns out I was
> wrong.
> http://bugs.racket-lang.org/query/?cmd=view%20audit-trail&database=default&pr=14506&return_url=http%3A%2F%2Fbugs.racket-lang.org%2Fquery%2F%3Fdatabase%3Ddefault%3Bdebug%3D%3BState%3Dany%3BSynopsis%3DVector%3Bmultitext%3D%3Bcolumns%3DState%3Bcolumns%3DSynopsis%3Bcolumns%3DCategory%3Bcolumns%3DLast-Modified%3Bcolumns%3DRelease%3Bcmd%3Dsubmit%2520query%3Bsortby%3DNumber
>
> On May 30, 2014, at 10:17 AM, Greg Hendershott
> <greghendershott at gmail.com <mailto:greghendershott at gmail.com>> wrote:
>
>> p.s. I happened to paste the error message from 5.3.5. The TR error
>> message format in recent versions of Racket is much nicer; kudos!
>>
>> ; /tmp/tr.rkt:4:8: Type Checker: type mismatch
>> ;   expected: (Sequenceof
>> ;              (U (Vector Any Any (U Real False ivl))
>> ;                 (List Any Any (U Real False ivl))))
>> ;   given: (List
>> ;           (Vector Symbol Symbol Integer)
>> ;           (Vector Symbol Symbol Integer)
>> ;           (Vector Symbol Symbol Integer))
>> ;   in: (discrete-histogram3d (quote (#(a a 1) #(a b 2) #(b b 3)))
>> #:label "Missing (b,a)" #:color 4 #:line-color 4)
>>
>>
>> On Fri, May 30, 2014 at 10:13 AM, Greg Hendershott
>> <greghendershott at gmail.com <mailto:greghendershott at gmail.com>> wrote:
>>> This example from the plot docs works great:
>>>
>>>    #lang racket
>>>    (require plot)
>>>    (plot-new-window? #t)
>>>    (plot3d (discrete-histogram3d '(#(a a 1) #(a b 2) #(b b 3))
>>>                                    #:label "Missing (b,a)"
>>>                                    #:color 4 #:line-color 4))
>>>
>>> But not with Typed Racket:
>>>
>>>    #lang typed/racket   ;<- typed
>>>    (require plot/typed) ;<- typed
>>>    (plot-new-window? #t)
>>>    (plot3d (discrete-histogram3d '(#(a a 1) #(a b 2) #(b b 3))
>>>                                    #:label "Missing (b,a)"
>>>                                    #:color 4 #:line-color 4))
>>>    ; /tmp/tr.rkt:7:8: Type Checker: Expected (Sequenceof (U (Vector
>>> Any Any (U Real False ivl)) (List Any Any (U Real False ivl)))), but
>>> got (List (Vector Symbol Symbol Integer) (Vector Symbol Symbol
>>> Integer) (Vector Symbol Symbol Integer))
>>>    ;   in: (discrete-histogram3d (quote (#(a a 1) #(a b 2) #(b b 3)))
>>> #:label "Missing (b,a)" #:color 4 #:line-color 4)
>>>
>>> It fails to typecheck on 6.0.1.10, but also back on 5.3.5.
>>>
>>> I don't understand the error; a list is a sequence, no?
>> ____________________
>>  Racket Users list:
>> http://lists.racket-lang.org/users
>
>
>
> ____________________
>    Racket Users list:
>    http://lists.racket-lang.org/users
>