TR: Occurrence Typing with custom predicate

[mmcdan]

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?

[Ben Greenman]

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`.

[mmcdan]

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!