A new way to type mutable data structures with opposite variance in typed racket

Show & Tell
1

Hi everyone,

I have been experimenting with a way to define types with opposite variance in typed racket (see also Is it possible to make Mutable Types support subtype? · racket/typed-racket · Discussion #1129 · GitHub). The idea is to use a struct with two type arguments, one for the input type and one for the output type, and then use a Parameter type to constrain them. For example, here is how I defined a type for queue, a mutable data structure from data/queue:

#lang typed/racket/base

(require typed/racket/unsafe)

(struct (S T) Queueof ([_ : (Parameter S T)]))
(define-type (Queue S T) (Queueof S T)) ; avoid printing #(struct:Queueof ...)
;; TODO (Queue T) -> (Queue T T)
#;(struct (A ...) _ ([_ : (Parameter A ...)]) #:type-name Queue) ; not work well
(provide Queue)

(unsafe-require/typed/provide
 data/queue
 [make-queue (All (S T) (-> (Queue S T)))]

 [enqueue! (All (S) (-> (Queue S Any) S Void))]
 [enqueue-front! (All (S) (-> (Queue S Any) S Void))]
 [dequeue! (All (T) (-> (Queue Nothing T) T))]

 [queue->list (All (T) (-> (Queue Nothing T) (Listof T)))]
 [queue-length (-> (Queue Nothing Any) Index)]

 [queue? (pred (Queue Nothing Any))]
 [queue-empty? (-> (Queue Nothing Any) Boolean)]
 [non-empty-queue? (All (S T)
                        (case->
                         (-> (Queue S T) Boolean)
                         (-> Any Boolean : #:+ (Queue Nothing Any))))])

I think this way of defining types with opposite variance is interesting and useful for mutable data structures. I wonder if it is safe to use, and if it is, can we redefine some built-in mutable types in this way? For example, can we redefine mutable vector or mlist in this way?

3 Likes