Read-write types

The Cons (and read-write semantics) page will tell you that two cons variants exist: Cons and &Cons. However, this is only the tip of the iceberg. If you find the definition of the Cons type in et.el, it shows that Cons is merely an alias to the underlying ConsRW type.

(et-defalias Cons [(L = Any) (R = Any)]
  (ConsRW L L R R))

ConsRW takes four arguments (CAR-READ CAR-WRITE CDR-READ CDR-WRITE).
In short, CAR-WRITE/CDR-READ can be thought of as the result of running (car/cdr CONS), and CAR-WRITE/CDR-WRITE can be thought of as the type for the second parameter of (setcar/setcdr CONS __).
By necessity, CAR-WRITE must be a subtype of CAR-READ (and likewise for CDR), because if you can write a value with type T to a particular slot, then the next read will necessarily get a value of type T. Thus, each pair (READ, WRITE) can be thought of as "the range of types from WRITE up to READ", with Never <: WRITE <: READ <: Any.

Subtyping

As might be expected, ConsRW is covariant in its read types and contravariant in its write types. In other words, if A and B are cons types, then

A <: B iff
  CAR-READ-A  <: CAR-READ-B
  CAR-WRITE-A :> CAR-WRITE-B
  CDR-READ-A  <: CDR-READ-B
  CDR-WRITE-A :> CDR-WRITE-B

As shown above with Cons, the standard (invariant) form of a type is defined by making the READ and WRITE type identical.
The read-only (covariant) form of a type on the other hand is defined by setting making the write type Never. In fact, read-only aliases are generated by performing the following two transformations:

1. Modify all RW types so that the WRITE type is Never
2. Replace all nested aliases with its read-only equivalent

A write-only (contravariant) form of a type can be defined by setting READ=Any. While setting WRITE=Never clearly means "you cannot write to this slot", it is less clear why READ=Any implies write-only. A more accurate characterization would be "when you read from this slot, you have no idea what will come out."

Other containers

Plists, vectors, and hash tables are all defined in terms of read-write types.

(et-defsyntax Plist (&rest args)
  (when (eq 1 (mod (length args) 2))
    (error "Plist must have an even number of arguments"))
  (cl-loop for (key type) on args by #'cddr
           nconc (list key type type) into rw-args
           finally return `(PlistRW ,@rw-args)))

(et-defalias Vector [(E = Any)] VectorRW<E_E>)
(et-defalias VectorW [E] VectorRW<Any_E>)

(et-defalias HashTable [(K = Any) (V = Any)] HashTableRW<K_K_V_V>)
(et-defalias HashTableW [(K = Any) (V = Any)] HashTableRW<Any_K_Any_V>)

So you want a write-only list

Defining contravariant types becomes very tricky with nested cons-cells. For example, suppose we wanted to define a contravariant "write-only list". We would want such a type to have the following two properties:

List<T> <: ListW<T>
A <: B  ==>  ListW<B> <: ListW<A>   (contravariance)

The naive idea would be to copy the read-only version, but use the write slot instead of the read slot:

(et-defalias ConsW [L R] (ConsRW Any L Any R))
(et-defalias ListW1 [T]
  (or Nil (ConsW T ListW1<T>)))

(et-subtype? (et ConsW<Number_Number>) (et ConsW<Integer_Integer>))
;; -> t - the cons cell is contravariant
(et-subtype? (et ListW1<Number>) (et ListW1<Integer>))
;; -> nil - the list is not

The first cons in the list behaves as desired, however the second cons is stuck behind the write-only cdr of the first cons. In order to write to the second cons of a list, you must first access it, which means reading from the cdr of the first cons. Each step in the list is behind another contravaraint slot, giving ListW1 a bizarre "oscillating variance" behavior:

(ConsW A (ConsW B (ConsW C (ConsW D ...))))
;;     ^        ^        ^        ^
;;     |    Covariant    |    Covariant
;;  Contravariant   Contravariant

(et-subtype? (et (ConsW Number (ConsW Integer (ConsW Number (ConsW Integer Nil)))))
             (et (ConsW Integer (ConsW Number (ConsW Integer (ConsW Number Nil))))))
;; -> t

So just make the cdr invariant, right?

(et-defalias ListW2 [T]
  (or Nil (ConsRW T Any ListW2<T> ListW2<T>)))

(et-subtype? (et ListW2<Number>) (et ListW2<Integer>))
;; -> nil

This is much better than the previous example. We can now safely traverse the list, because we know that each cdr that we read will be another ListW2<T>. Furthermore, at each step, we can write a T to the car but not read one, just as desired.
The issue is that ListW2<Number> still fails to be a subtype of ListW2<Integer> in the CDR-WRITE slot, which prevents this definition from being contravariant.

If we make the cdr read-only, we finally get a contravariant type:

(et-defalias ListW3 [T]
  (or Nil (ConsRW Any T ListW3<T> Never)))

(et-subtype? (et ListW3<Number>) (et ListW3<Integer>))
;; -> t
(et-subtype? (et List<Number>) (et ListW3<Number>))
;; -> t

This has the obvious downside that a list with a read-only cdr cannot be appended to. The typesystem has good reason to block this kind of operation: the following example illustrates why appends are fundamentally dangerous on a contravariant list type.

(et-defvar my-num-list List<Number> '(0.1 0.2 0.3))
(et-defvar my-int-list List<Integer> '(1 2 3))

(et-defun nconc-ints (a: ListW<Integer> b: List<Integer>) Any
  (nconc a b))

(add-ints-to-list my-num-list my-int-list)
;; No problem yet, my-num-list just contains more numbers

(nconc my-nums-to-list (list 0.4))
;; my-int-list now contains a float

In this example, the problem is not with appends themselves, but with the shared references that result from them. Motivated by this observation, we can finally define the one write-only list to rule them all:

(et-defalias ListW [T]
  (or Nil (ConsRW Any T ListW<T> ListFresh<T>)))

(et-subtype? (et ListW<Number>) (et ListW<Integer>))
;; -> t
(et-subtype? (et List<Number>) (et ListW<Number>))
;; -> t

Hopefully you can now appreciate why contravariance is not simply "covariance in the other direction", but is rather far more intricate and complex to deal with.