I asked about this a few years ago but cannot find a reply. Does Typed Racket have mutable hash sets? If so, I can't figure out how to use them. In particular, mutable-seteq seems to be unavailable, not even to make an initially empty mutable hash set.
Typed Racket has no types for mutable sets because they are unsound, because mutable sets cannot be covariant.
To explain why:
#lang typed/racket/base
(require racket/set)
;; structs
(struct -animal ([species : String]) #:type-name Animal)
(struct -dog -animal ([name : String]) #:type-name Dog)
;; instances
(define coral (-animal "coral"))
(define fido (-dog "dog" "Fido"))
;; procedures
(: call-dog : Dog -> Void)
(define (call-dog dog)
(printf "Come here, ~a!~n" (-dog-name dog)))
(: point-out-animal : Animal -> Void)
(define (point-out-animal animal)
(printf "Look, that's a ~a.~n" (-animal-species animal)))
;; show that procedures can only be called with their types
(point-out-animal coral)
(point-out-animal fido)
;; (call-dog coral) -> type checker error because Animal is not a Dog
(call-dog fido)
(: dogs (Setof Dog))
(define dogs (set fido)) ;; only Dog can go in (Setof Dog)
(: all-animals (Setof Animal))
(define all-animals (set coral fido)) ;; any Animal, including Dog, can go in (Setof Animal)
(: some-animals (Setof Animal))
(define some-animals dogs) ;; a (Setof Dog) can be stored in a (Setof Animal) variable, because a Dog is still an Animal
#|
Now imagine if these sets were mutable sets.
(set-add! some-animals coral)
This would pass the type checker because a coral is an Animal and can be added to (Setof Animal)
However, doing this would be unsound.
The coral would be added to some-animals which is the same mutable set as dogs. But dogs is a (Setof Dog), and you just added a non-dog to it.
That means taking items out of dogs, which is typed as a (Setof Dog), might not actually give you a Dog.
Want to try it? Set the #lang to typed/racket/base/no-check and uncomment the following block. It will fail at runtime with:
; -dog-name: contract violation
; expected: -dog?
; given: #<-animal>
; Context (errortrace):
; covariant.rkt:15:29: (-dog-name dog)
|#
#;(begin
(set! dogs (mutable-set fido))
(set! some-animals dogs)
(set-add! some-animals coral))
;; With immutable sets, this is sound. With mutable sets, there's no guarantees, so standard Typed Racket won't let you create mutable sets.
(displayln " -- Calling all dogs:")
(for ([dog dogs])
(call-dog dog))
1 Like
I don't need covariance. I don't care if a set of dog is a set of animal,
as long as it is a set of dog. I don't expect a mutable setof dog to be a
mutable set of animal. I just need it to be a set of dog.
Shouldn't that be possible?
The same argument would apply to a variable of type dog. It should not
be treated as a variable of type animal, even though dogs are animals.
Nor should a struct containing a mutable dog field be used as a struct
containing a mutable animal field.
I just want to be able to have a mutable set of dog, not a mutable
set of animal.
I first encountered noncovariant inheritance in the language Eiffel, and
consider it to be a categorical error that should never have been part
of the language.
-- hendrik
2 Likes
I don't expect a mutable setof dog to be a
mutable set of animal. [...] It should not
be treated as a variable of type animal, even though dogs are animals.
Typed Racket does treat mutable hash tables this way, so if it's an option for you, you could use hash tables instead of sets, and just ignore the value of the hash table. Here, I've used False as a placeholder:
#lang typed/racket/base
;; structs
(struct -animal ([species : String]) #:type-name Animal)
(struct -dog -animal ([name : String]) #:type-name Dog)
;; instances
(define coral (-animal "coral"))
(define fido (-dog "dog" "Fido"))
;; hash tables
(: dogs (Mutable-HashTable Dog False))
(define dogs (make-hash `((,fido . #f)))) ;; only Dog can go in (Mutable-HashTable Dog False)
(: all-animals (Mutable-HashTable Animal False))
(define all-animals (make-hash `((,fido . #f) (,coral . #f)))) ;; any Animal, including Dog, can go in (Mutable-HashTable Animal False)
;; Typed Racket does not allow mutable hashtables to be covariant.
(: some-animals (Mutable-HashTable Animal False))
(define some-animals dogs) ;; -> Type Checker: type mismatch: expected (Mutable-HashTable Animal False), given (Mutable-HashTable Dog False)
Alternatively, if you use immutable sets and operators like set-add, there's no problem. Typed Racket knows that if you (set-add dogs fido) the return value is a (Setof Dog), and if you (set-add dogs coral) the return value is a (Setof Animal). The drawback of using immutable sets is you need to be more familiar with the language builtins to know how you can manipulate data. One such builtin is for/set, though I find myself using recursion with named let more often.
Even if mutable sets worked the way you wanted, I think you'd need to learn these techniques anyway, to be able to deal with data that's always immutable like strings.
Kotlin has an interesting and intuitive solution to variance, where they have "in" and "out" types for generics. We don't have a comparable idea in Typed Racket.
Why couldn't (define some-animals dogs) raise a type error when using mutable sets? That's definitely an error and should be treated as one, just like it is for mutable hash tables.
You could definitely propose something like that.
I notice there's an out of date GitHub issue about this too: Typed Racket pretends mutable sets don't exist, and yet it assumes all hashtables could be mutable · Issue #32 · racket/typed-racket · GitHub
I think we can use Parameter and struct to define mutable types that support contravariance. See A new way to type mutable data structures with opposite variance in typed racket.
1 Like