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🔗ℹ

2.1 Defining Record Types🔗ℹ

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

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

descriptor-spec = <this>
| (<this> #f)
| (<this> <super>)

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.
descriptor-spec specifies the record type descriptor name (in angle brackets like <this>) and optional <super>:
- <this> or (<this> #f): defines a new base record type.
- (<this> <super>): defines a record type that inherits from super, 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 this that optionally extends super.
Type aliases (if the type parameters are not ()):
- thisTop: all parameters at their top bound (e.g., Any for covariant, Nothing for contravariant).
- thisBot: all parameters at their bottom bound (e.g., Nothing for covariant, Any for contravariant).
A macro <this>: (<this>) expands to the record type descriptor, and (<this> (f e ...)) expands to (f e ... <super> field-spec ...).
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.

2.1.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

2.1.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

2.2 Base Record Type🔗ℹ

type
record

Any record type value.

type
Record-TypeTop

Any record type descriptor value.

procedure
(record? v) → Boolean
v : Any

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

Examples:

> (:print-type record?)
(-> Any Boolean : record)
> (define-record-type <example> (make-example) example?)
> (:print-type make-example)
(-> example)
> (:print-type example?)
(-> Any Boolean : example)
> (record? (make-example))
- : True
#t

procedure
(record-type-descriptor? v) → Boolean
v : Any

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

Examples:

> (:print-type record-type-descriptor?)
(-> Any Boolean : Record-TypeTop)
> (define-record-type <example> #f #f)
> (record-type-descriptor? (<example>))
- : True
#f

procedure
(record-type-descriptor rt) → Record-TypeTop
rt : record

Given a record type instance rt, returns its descriptor.

Examples:

> (:print-type record-type-descriptor)
(-> record Record-TypeTop)
> (define-record-type <example> (make-example) #f)
> (record-type-descriptor (make-example))
- : Record-TypeTop
#<struct-type:example>

procedure
(record-type-parent rtd) → (Option Record-TypeTop)
rtd : Record-TypeTop

Returns the parent record type descriptor of rtd, or #f if there is no parent.

Examples:

> (:print-type record-type-parent)
(-> Record-TypeTop (U False Record-TypeTop))
> (define-record-type <example> #f #f)
> (record-type-parent (<example>))
- : (U False Record-TypeTop)
#f
> (define-record-type (<instance> <example>) #f #f)
> (record-type-parent (<instance>))
- : (U False Record-TypeTop)
#<struct-type:example>

procedure
(record-type-name rtd) → Symbol
rtd : Record-TypeTop

Returns the name of the record type represented by rtd.

Examples:

> (:print-type record-type-name)
(-> Record-TypeTop Symbol)
> (define-record-type <example> #f #f)
> (record-type-name (<example>))
- : Symbol
'example

procedure
(record-type-constructor rtd) → Procedure
rtd : Record-TypeTop

Returns a constructor procedure to create instances of the type for record type.

Examples:

> (:print-type record-type-constructor)
(-> Record-TypeTop Procedure)
> (define-record-type <example> #f #f)
> (record-type-constructor (<example>))
- : Procedure
#<procedure:make-example>

procedure
(record-type-predicate rtd) → Procedure
rtd : Record-TypeTop

Returns a predicate procedure to recognize instances of the type for record type.

Examples:

> (:print-type record-type-predicate)
(-> Record-TypeTop Procedure)
> (define-record-type <example> #f #f)
> (record-type-predicate (<example>))
- : Procedure
#<procedure:p>

procedure
(record-type-fields rtd)
→ (Listof (List Symbol Procedure Procedure))
rtd : Record-TypeTop

Returns a list describing the fields of the record type rtd. Each field is represented as a list of three elements:

A symbol representing the field name (warning: this feature is not currently supported).
An accessor procedure for reading the field value.
A mutator procedure for writing the field value.

Examples:

> (:print-type record-type-fields)
(-> Record-TypeTop (Listof (List Symbol Procedure Procedure)))
> (define-record-type <example>
    (make-example [v1 : Integer Natural] [v2 : Symbol])
    #f
    [v2 get-v2]
    [v1 get-v1 set-v1!])
> (record-type-fields (<example>))
- : (Listof (List Symbol Procedure Procedure))
'((unknown139133 #<procedure:get> #<procedure:set>)
  (unknown139133 #<procedure:get> #<procedure:set>))

procedure
(make-record-type-descriptor name
fieldspecs) → Record-TypeTop
  name : Symbol
  fieldspecs : (Listof (∪ Symbol (List (∪ 'immutable 'mutable) Symbol)))
(make-record-type-descriptor name
fieldspecs
super-type) → Record-TypeTop
  name : Symbol
  fieldspecs : (Listof (∪ Symbol (List (∪ 'immutable 'mutable) Symbol)))
  super-type : Record-TypeTop

Creates a new record type descriptor with the given name, field specifications fieldspecs, and optional parent descriptor super-type.

Each element of fieldspecs can be:

name or (list 'immutable name), representing an immutable field.
(list 'mutable name), representing a mutable field.

Examples:

> (:print-type make-record-type-descriptor)
(->* (Symbol (Listof (U (List (U 'immutable 'mutable) Symbol) Symbol)))
(Record-TypeTop)
Record-TypeTop)
> (make-record-type-descriptor 'example '())
- : Record-TypeTop
#<struct-type:example>

procedure
(make-record rtd field-vector) → record
rtd : Record-TypeTop
field-vector : VectorTop

Creates a new record type instance of the described by rtd, with field values taken from field-vector. field-vector must contain exactly one value for each field in the record type (including inherited fields).

Examples:

> (:print-type make-record)
(-> Record-TypeTop VectorTop record)
> (define-record-type <example> #f #f)
> (make-record (<example>) #())
- : record
#<example>