Typed SRFI 136: Extensible Record Types with Variance Annotations🔗ℹ

1 Introduction🔗ℹ

This library provides a typed version of SRFI 136 (Extensible Record Types) for Typed Racket, with support for variance annotations on type parameters. It extends SRFI 9 by adding inheritance, allowing you to define record types that extend existing 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 API Reference🔗ℹ

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

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

type-spec = type-name
| (type-name #f)
| (type-name parent)

constructor-spec = #f
| (constructor-name field-tag ...)

predicate-spec = #f
| predicate-name

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

field-spec = [field-name accessor-name]
| [field-name accessor-name mutator-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-spec specifies the record type name and optional parent:
- type-name or (type-name #f): defines a new base record type.
- (type-name parent): defines a record type that inherits from parent, including all its fields
constructor-name is the name of the constructor procedure. If #f, no constructor is generated.
A field-tag specifies a field.
- An immutable field has the form [field-name : read-type].
- A mutable field has the form [field-name : read-type write-type].
- When inheriting, you must specify all fields, including the inherited fields.
predicate-name is the name of the predicate procedure. If #f, no predicate is generated.
A field-spec specifies the accessor and optional mutator:
- An immutable field has only an accessor.
- A mutable field has both an accessor and a mutator.
- When inheriting, you only specify the new fields added by this record type, not the inherited fields.

This form defines the following:

A struct type named type-name that optionally extends parent.
Type aliases (if the type parameters are not ()):
- 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 (if not #f) to create instances. 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 (if not #f) that tests for type-nameTop.
An accessor-name for each specified field.
A mutator-name for each specified mutable field.

procedure
(record? v) → Boolean
v : Any

Returns #t if v is an instance of a record, #f otherwise.

Example:

> (:print-type record?)
(-> Any Boolean : <record>)

3 Examples🔗ℹ

3.1 Mutable Boxes and Pairs🔗ℹ

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 #(struct:Mutable-Box ((case-> (-> t1) (-> t1 Void))))))
> (:print-type BOX?)
(-> Any Boolean : Mutable-BoxTop)
> (:print-type UNBOX)
(All (+t1)
  (-> #(struct:Mutable-Box ((case-> (-> +t1) (-> Nothing Void)))) +t1))
> (:print-type SET-BOX!)
(All (-t1)
  (-> #(struct:Mutable-Box ((case-> (-> Any) (-> -t1 Void)))) -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)
  (-> #(struct:Mutable-Box ((case-> (-> t1) (-> t1 Void))))
      #(struct:Mutable-Box ((case-> (-> t2) (-> t2 Void))))
      #(struct:Mutable-Pair
        ((-> #(struct:Mutable-Box ((case-> (-> t1) (-> t1 Void)))))
         (-> #(struct:Mutable-Box ((case-> (-> t2) (-> t2 Void)))))))))
> (:print-type MPAIR?)
(-> Any Boolean : Mutable-PairTop)
> (:print-type get-b1)
(All (-t1 +t1)
  (-> #(struct:Mutable-Pair
        ((-> #(struct:Mutable-Box ((case-> (-> +t1) (-> -t1 Void)))))
         (-> Mutable-BoxTop)))
      #(struct:Mutable-Box ((case-> (-> +t1) (-> -t1 Void))))))
> (:print-type get-b2)
(All (-t2 +t2)
  (-> #(struct:Mutable-Pair
        ((-> Mutable-BoxTop)
         (-> #(struct:Mutable-Box ((case-> (-> +t2) (-> -t2 Void)))))))
      #(struct:Mutable-Box ((case-> (-> +t2) (-> -t2 Void))))))
> (: 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

3.2 Inheritance🔗ℹ

A hierarchy of point types with increasingly dimensions:

Examples:

> (define-record-type Point #f #f)
> (define-record-type () (Point-0 Point)
    (make-point-0)
    point-0?)
> (:print-type make-point-0)
(-> Point-0)
> (:print-type point-0?)
(-> Any Boolean : Point-0)
> (define p0 (make-point-0))
> (point-0? p0)
- : True
#t
> (define-record-type (-t1 +t1) (Point-1 Point-0)
    (make-point-1 [p1 : +t1 -t1])
    point-1?
    [p1 get-p1 set-p1!])
> (:print-type make-point-1)
(All (t1) (-> t1 #(struct:Point-1 ((case-> (-> t1) (-> t1 Void))))))
> (:print-type point-1?)
(-> Any Boolean : Point-1Top)
> (:print-type get-p1)
(All (+t1) (-> #(struct:Point-1 ((case-> (-> +t1) (-> Nothing Void)))) +t1))
> (:print-type set-p1!)
(All (-t1) (-> #(struct:Point-1 ((case-> (-> Any) (-> -t1 Void)))) -t1 Void))
> (define p1 (make-point-1 1))
> (point-0? p1)
- : True
#t
> (point-1? p1)
- : True
#t
> (get-p1 p1)
- : Integer
1
> (set-p1! p1 -1)
> (get-p1 p1)
- : Integer
-1
> (define-record-type (-t1 +t1 -t2 +t2) (Point-2 Point-1)
    (make-point-2 [p1 : +t1 -t1] [p2 : +t2 -t2])
    point-2?
    [p2 get-p2 set-p2!])
> (:print-type make-point-2)
(All (t1 t2)
  (-> t1
      t2
      #(struct:Point-2
        ((case-> (-> t1) (-> t1 Void)) (case-> (-> t2) (-> t2 Void))))))
> (:print-type point-2?)
(-> Any Boolean : Point-2Top)
> (:print-type get-p2)
(All (+t2)
  (-> #(struct:Point-2
        ((case-> (-> Any) (-> Nothing Void))
         (case-> (-> +t2) (-> Nothing Void))))
      +t2))
> (:print-type set-p2!)
(All (-t2)
  (-> #(struct:Point-2
        ((case-> (-> Any) (-> Nothing Void)) (case-> (-> Any) (-> -t2 Void))))
      -t2
      Void))
> (define p2 (make-point-2 1 2))
> (point-0? p2)
- : True
#t
> (point-1? p2)
- : True
#t
> (point-2? p2)
- : True
#t
> (get-p1 p2)
- : Integer
1
> (set-p1! p2 -1)
> (get-p1 p2)
- : Integer
-1
> (get-p2 p2)
- : Integer
2
> (set-p2! p2 -2)
> (get-p2 p2)
- : Integer
-2