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
#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?