Typed SRFI 9: Defining Record Types with Variance Annotations🔗ℹ

1 Introduction🔗ℹ

This library provides a typed version of SRFI 9 (Defining Record Types) for Typed Racket, with support for variance annotations on type parameters. It allows you to define record types with precise control over the variance of mutable and immutable fields.

Variance determines how subtyping relationships between type parameters affect subtyping of the parameterized type:

Contravariant positions reverse subtyping order: if a is a subtype of b, then (F b) is a subtype of (F a).
Covariant positions preserve subtyping order: if a is a subtype of b, then (F a) is a subtype of (F b).

For a record type (F w r), if w is a contravariant position and r is a covariant position, the type (F w2 r2) is a subtype of (F w1 r1) if and only if:

w1 is a subtype of w2
r2 is a subtype of r1

2 Syntax🔗ℹ

syntax
(define-record-type maybe-type-vars type-name
  (constructor-name field-tag ...)
  predicate-name
  field-spec ...)

maybe-type-vars = (v ...)

field-tag = [field-name : write-type read-type]
| [field-name : read-type]

field-spec = [field-name accessor-name mutator-name]
| [field-name accessor-name]

Defines a new record type with optional type parameters and variance annotations.

v is a type parameter. It uses prefix notation to indicate variance:
- - prefix (e.g., -t): Contravariant parameter. Top type is Nothing, bottom type is Any.
- + prefix or no prefix (e.g., +t or t): Covariant parameter. Top type is Any, bottom type is Nothing.
type-name is the name of the new record type.
constructor-name is the name of the constructor procedure.
A field-tag specifies a field.
- An immutable field has the form [field-name : read-type].
- A mutable field has the form [field-name : write-type read-type].
predicate-name is the name of the predicate procedure.
A field-spec specifies the accessor and optional mutator. An immutable field has an accessor, while a mutable field has both an accessor and a mutator.

This form defines the following:

A struct type named type-name.
Type aliases:
- type-nameTop: all parameters at their top bound (e.g., Any for covariant, Nothing for contravariant).
- type-nameBot: all parameters at their bottom bound (e.g., Nothing for covariant, Any for contravariant).
A constructor-name procedure to create instances of the record. For mutable fields, the write-type must be a subtype of the read-type. To satisfy this subtyping constraint from the very beginning in the simplest way, the variance prefixes (- and +) are stripped from the type parameters when generating the constructor’s type.
A predicate-name procedure (predicate for type-nameTop).
An accessor-name for each field.
A mutator-name for each mutable field.

3 Examples🔗ℹ

A simple mutable box demonstrating variance, and a mutable pair composed from mutable boxes, illustrating how variance propagates through nested data structures. The type (Mutable-Box Natural Integer) means:

You can write values of type Natural (or any subtype) into the box, demonstrating contravariance of the write type.
You can read values of type Integer (or any supertype) from the box, demonstrating covariance of the read type.

Examples:

> (define-record-type (-t1 +t1) Mutable-Box
    (BOX [v : -t1 +t1])
    BOX?
    [v UNBOX SET-BOX!])
> (:print-type BOX)
(All (t1) (-> t1 (Mutable-Box t1 t1)))
> (:print-type BOX?)
(-> Any Boolean : Mutable-BoxTop)
> (:print-type UNBOX)
(All (+t1) (-> (Mutable-Box Nothing +t1) +t1))
> (:print-type SET-BOX!)
(All (-t1) (-> (Mutable-Box -t1 Any) -t1 Void))
> (: b (Mutable-Box Natural Integer))
> (define b (BOX -111))
> (BOX? (ann b (Mutable-Box Byte Number)))
- : True
#t
> (UNBOX b)
- : Integer
-111
> (SET-BOX! b 0)
> (UNBOX b)
- : Integer
0
> (define-record-type (-t1 +t1 -t2 +t2) Mutable-Pair
    (make-mpair [b1 : (Mutable-Box -t1 +t1)]
                [b2 : (Mutable-Box -t2 +t2)])
    MPAIR?
    [b2 get-b2]
    [b1 get-b1])
> (:print-type make-mpair)
(All (t1 t2)
  (-> (Mutable-Box t1 t1) (Mutable-Box t2 t2) (Mutable-Pair t1 t1 t2 t2)))
> (:print-type MPAIR?)
(-> Any Boolean : Mutable-PairTop)
> (:print-type get-b1)
(All (-t1 +t1) (-> (Mutable-Pair -t1 +t1 Nothing Any) (Mutable-Box -t1 +t1)))
> (:print-type get-b2)
(All (-t2 +t2) (-> (Mutable-Pair Nothing Any -t2 +t2) (Mutable-Box -t2 +t2)))
> (: MCONS (∀ (t1 t2) (→ t1 t2 (Mutable-Pair t1 t1 t2 t2))))
> (define (MCONS v1 v2) (make-mpair (BOX v1) (BOX v2)))
> (: MCAR (∀ (+t1) (→ (Mutable-Pair Nothing +t1 Nothing Any) +t1)))
> (: MCDR (∀ (+t2) (→ (Mutable-Pair Nothing Any Nothing +t2) +t2)))
> (define (MCAR p) (UNBOX (get-b1 p)))
> (define (MCDR p) (UNBOX (get-b2 p)))
> (: SET-MCAR! (∀ (-t1) (→ (Mutable-Pair -t1 Any Nothing Any) -t1 Void)))
> (: SET-MCDR! (∀ (-t2) (→ (Mutable-Pair Nothing Any -t2 Any) -t2 Void)))
> (define (SET-MCAR! p v1) (SET-BOX! (get-b1 p) v1))
> (define (SET-MCDR! p v2) (SET-BOX! (get-b2 p) v2))
> (: p (Mutable-Pair Natural Integer Zero Byte))
> (define p (MCONS -1 1))
> (MPAIR? (ann p (Mutable-Pair Byte Number Nothing Natural)))
- : True
#t
> (MCAR p)
- : Integer
-1
> (SET-MCAR! p 1)
> (MCAR p)
- : Integer
1
> (MCDR p)
- : Integer [more precisely: Byte]
1
> (SET-MCDR! p 0)
> (MCDR p)
- : Integer [more precisely: Byte]
0