Hello Ben, Good call. I didn't think about the mutability of the container's contents with respect to types. My goal is to create a type that represents an immutable container.
After exploring, it looks like there is a workaround: In the case of Vector, I can create a struct to hold the vector-immutable. In the case of Box, the struct can itself can be considered the box. The struct automatically generates the occurrence type predicate. --- #lang typed/racket (struct VoS ([contents : (Immutable-Vectorof Symbol)])) (define test-vos (VoS (vector-immutable 'A))) (VoS? test-vos) ;; #t (VoS-contents test-vos) ;; '#(A) --- I'll start using structs more often, instead of the *of types directly. Thanks! On Tuesday, March 24, 2020 at 3:50:39 PM UTC-7, Ben Greenman wrote: > > On 3/24/20, mmcdan <mmcda...@gmail.com <javascript:>> wrote: > > Hello, > > > > I'm trying to use occurrence typing for (Vectorof Symbol) or (Boxof > > Symbol). > > > > Creating a custom predicate for (Listof Symbol) seems to work: > > --- > > #lang typed/racket > > > > (: los? (-> Any Boolean : (Listof Symbol))) > > (define los? > > (lambda (seq) (and (list? seq) (andmap symbol? seq)))) > > --- > > > > However I haven't been able to create one for vectors or boxes. None of > the > > things I've tried will typecheck. Any pointers? > > Typed Racket can't be sure that untyped code won't change whats inside > a mutable vector or box > > --- > #lang racket > (define v (vector 'A)) > (define (set-v!) (vector-set! v 0 0)) > (provide v set-v!) > > #lang typed/racket > (require/typed "path-to-untyped.rkt" > (v : (Vectorof Any)) > (set-v! : (-> Void))) > > ;; suppose this worked > (: vos (-> Any Boolean : (Vectorof Symbol))) > (define (vos x) ....) > > (cond > [(vos? v) > ;; v : (Vectorof Symbol) > (set-v!) > ;; v now contains an integer! > ....])) > --- > > I don't know a work-around. > > I was hoping it could work for (Immutable-Vectorof Symbol), but I > don't know what to use in place of `andmap`. > -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/a9b1f475-24df-4d05-b979-001763edd0c1%40googlegroups.com.
