Is it possible to make Mutable Types support subtype?

[NoahStoryM]

I tried to write mlength for mlist, but it can't work for (MPairof Natural Null) type:

(: mlength (-> (MListof Natural) Natural))
(define mlength
  (λ (m)
    (if (null? m)
        0
        (add1 (mlength (mcdr m))))))

(: mls (MPairof Natural Null))
(define mls (mcons 9 '()))


(mlength mls)

I can understand it: (MPairof Natural Null) is not subtype of (MListof Natural)
because we can't run (set-mcdr! mls (ann (mcons 8 '()) (MListof Natural))).
But it's legal for mlength to run (set-mcdr! m (ann (mcons 8 '()) (MListof Natural)))
in its body when mls bound to m, which cause conflict.

I wonder if it's possible to make Mutable Types support subtype, and when TR
found conflict, just throw an exception?
(I haven't studied type theory, I just wonder if it's feasible?)

for example:

(: mls (MListof Natural))
(define mls (mcons 9 '()))

(: change-1st! (-> (MListof Any) #:immediately Void))
(define change-1st!
  (λ (mls)
    (unless (null? mls)
      (set-mcar! mls 'sym))))

(displayln mls)
(change-1st! mls)
(displayln mls)

when apply mls to change-1st!, it will record mls's type and value.
If mls's type is changed, then TR throws an exception.
(typecheck happens when the Mutable Type's assign operator was applied if the keyword is #:immediately,
or it happens when the calculation is finished if the keyword is #:end,
or it doesn't happen if the keyword is #:never)

[samth]

This is a possible language design -- it's roughly how the array type in Java works. When you create an array in Java, it records the type it's supposed to have, and if you try to assign something wrong to it then there's a runtime error. So we could have a design where mutable pairs recorded the types of their two fields when they were created, and did runtime checks for those types on assignment. Then we would have covariant subtyping on mutable pairs.

Unfortunately, this is a very different design than what Racket has today, so it would make it impossible for mpairs in Typed Racket to be the same as mpairs in Racket. That's a reasonable choice for a language, but Typed Racket aims to be highly-compatibly with Racket, so it won't work for Typed Racket.

I'm going to move this to a "discussion" because that seems like a better place for discussing possible options for programs like this.

[NoahStoryM]

I see. In addition, I am a little curious that there are many restrictions on the use of mutable types in TR (for example, it is impossible to define predicate for them). Are these restrictions mainly due to subtypes?

[samth]

These are indeed related issues. Consider this program:

(define-predicate p? (MPair Integer Integer))
(define v : (MPair Any Any) (mcons 1 2))

(if (p? v) (+ 1 (mcar v)) 2)

Should this type check? Unfortunately, it can't, because in between the (p? v) and the (mcar v), someone else could do (set-mcar! v 'x) and then we'd have a type error.

The fundamental issue is that subtyping (or rather, covariance) is possible only when your code is making that choice of the subtype. But when you have a channel of communication from someone else, as in a function result or reading the value of a mutable location, then that someone else is making the choice of the subtype, so you can't know which one it's going to be.

[AlexKnauth]

If every type-argument in a mutable type constructor were replaced with a pair of types with opposite variance, we could get something. I'll use (Boxof t) as an example. If we replace that t with a pair of types, t- and t+, then we get subtyping like this:

b- <: a-     and     a+ <: b+
------------------------------
(Boxof a- a+) <: (Boxof b- b+)

In other words in (Boxof t- t+), t- is contravariant while t+ is covariant. The type t- represents the types that may be written into the box with set-box!, and the type t+ represents the types that may be read from the box with unbox.

The box/c contract combinator already supports this:

> (contract-stronger? (box/c exact-integer? exact-integer?)
                      (box/c exact-integer? any/c))
#t
> (contract-stronger? (box/c exact-integer? exact-integer?)
                      (box/c any/c any/c))
#f

---

For the example above with MPairof, no, (MPairof Natural Null) should still not be a subtype of (MListof Natural), but replacing each type with a pair of types written as (t-, t+), would give:

(MPairof (Natural, Natural) ((MListof (Natural, Natural)), Null)) <: (MListof (Natural, Natural))

This would also allow a more expressive type for mlength that says that it can't mutate the mlist its given... in other words it would allow read-only versions of mutable types:

(define-type (ReadOnlyMListof t)
  (U Null (MPairof (Nothing, t) (Nothing, (ReadOnlyMListof t)))))

(: mlength (-> (ReadOnlyMListof Natural) Natural))

And then with that more expressive type the new mlength can be called with an (MPairof Natural Null) with no problem because:

(MPairof (Natural, Natural) (Null, Null)) <: (MPairof (Nothing, Natural) (Nothing, (ReadOnlyMListof Natural)))
--------------------------------------------------------------------------------------------------------------
(MPairof (Natural, Natural) (Null, Null)) <: (ReadOnlyMListof Natural)

[NoahStoryM]

So (Parameter W R) is more similar to (case-> (-> W Void) (-> R)),
which is different from a box with dynamic scope? When it needs input,
the input's type must be W?

But if there are a type like dynamic scope box, and an operator dynamic-box,
should the binding type be W or R?

For example:

(: b1 (Dynamic-Immutable-Boxof Natural))
(define b1 (dynamic-immutable-box 1))

(: b2 (Dynamic-Boxof Natural Number))
(define b2 (dynamic-box -1))

(unbox b1) ; 1
(unbox b2) ; -1

(dynamic-box ([b1 0]
              [b2 val]  ; should val be W type (Natural) or R type (Number)?
              )
  (unbox b1) ; 0
  (unbox b2) ; val
  
  (set-box! b2 2)
  (unbox b2) ; 2
  )

(unbox b1) ; 1
(unbox b2) ; -1

I guess I know where I got it wrong:

• From racket guide:
  The parameterize form is not a binding form like let; each use of location above refers directly to the original definition. A parameterize form adjusts the value of a parameter during the whole time that the parameterize body is evaluated, even for uses of the parameter that are textually outside of the parameterize body:

parameterize is not similar to let, dynamic-box, it does not create a new reference:

(: p1 (Parameter Natural Number))
(define p1 (make-parameter -1))

(define p2 p1)

(parameterize ([p1 2]); adjusts the value of p1
   (displayln (eq? p1 p2)); #t
   )

(: b1 (Dynamic-Immutable-Boxof Natural))
(define b1 (dynamic-immutable-box 1))
(define b2 b1)

(unbox b1); 1
(unbox b2); 1

(dynamic-box ([b1 0]); create a new dynamic-immutable-box.
   (displayln (eq? b1 b2)); #f
   )

[AlexKnauth]

Would you have better understanding if we labeled them "Input" and "Output" instead of "Write" and "Read"? In (Boxof t- t+), the t- is the type used inputs, and t+ is the type used for outputs.

Or, since it's already using - and +, would you understand it better if we labeled them "Negative" and "Positive"? This is related to negative and positive blame for values crossing a contract boundary, if you're familiar with that.

[NoahStoryM]

I guess I could understand this. In my understanding, all operations on a subtype can also be performed on its supertype all operations on a supertype can also be performed on its subtype.
The two most typical operations are read and write. The supertype can safely read "more" types and write "fewer" types than its subtype.

So

a+ <: b+
------------------------------
(Boxof Nothing a+) <: (Boxof Nothing b+)

b- <: a-
------------------------------
(Boxof a- Nothing) <: (Boxof b- Nothing)

[AlexKnauth]

all operations on a subtype can also be performed on its supertype

Not quite, you have this part backwards: all operations on a supertype can also be performed on its subtype, so if you have (f b) where b : B, and A <: B, then (f a) should also typecheck where a : A. All operations on the supertype B can also be performed on its subtype A.

[NoahStoryM]

Thank you very much! I confused subtype and supertype before. (f a) and (f b) example is very easy to understand!

[samth]

In general, to look for more work on this topic, searching for "declaration site variance" vs "use-site variance" is the way to find papers, eg: https://dl.acm.org/doi/abs/10.1145/2489837.2489842

[NoahStoryM]

It seems that supporting write types is more difficult than contracts: https://racket.discourse.group/t/a-new-way-to-type-mutable-data-structures-with-opposite-variance-in-typed-racket/1846/7?u=noahstorym .