Cons (and read-write semantics)

The type (Cons A B) represents a cons cell with car A and cdr B. By default, the Cons type is invariant, meaning that cons types don't extend each other just because their argument types do. For example, a Cons<Integer_Integer> is not a valid Cons<Number_Number>. Consider the following situation:

(et-defun multiply-car (cons: Cons<Number_Any>) Nil
  (setcar cons (* 1.5 (car cons))))

(et-defvar integer-cons Cons<Integer_Integer> (cons 1 1))
(multiply-car integer-cons)
integer-cons
;; -> (1.5 . 1)

As shown, accepting a Cons<Integer_Integer> as a Cons<Number_Any> violates correctness, and must be rejected. In order to allow for covariance, we must define a read-only version of a cons cell, &Cons. A &Cons cannot be written to, so &Cons<Integer_Integer> is a subtype of &Cons<Number_Number> without violating correctness.
Furthermore, a standard cons can be a subtype of a read-only cons, but not the other way around. To understand why, think about each cons type as "supporting" certain operations:

	car	cdr
&Cons<A_B>	Read A	Read B
Cons<X_Y>	Read X, Write X	Read Y, Write Y

If X <: A and Y <: =B, then Cons<X_Y> supports all of the operations that &Cons<A_B> does. Thus, Cons<X_Y> <: &Cons<A_B>.

For readability, types containing Cons and &Cons types are often printed in compact lisp notation:

(et (Cons 1 (Cons 2 (Cons 3 Nil))))
;; -> (1 2 3)
(et &Cons<1_2>)
;; -> &(1 . 2)
(et (Cons 1 (&Cons 2 (&Cons 3 Nil))))
;; -> (1 . &(2 3))

The underlying Cons types still exist, but the formatter hides them for brevity.

For advanced details on the implementation of read-only types, see Read-write types.