Recursive types
Recursion lets us repeat a computation an arbitrary number of times, but we also want to be able to represent arbitrary collections of data. For example, you might want to represent the students in a class and write computations to compute average grades etc.
Bespoke lists
Suppose that we want to have lists of shapes?
Informally, we might think of a list of shapes as being either
-
an empty list
-
a pair of a shape and a list of shapes
This is an example of an inductively defined set. We can define such sets in Typed Racket as follows:
(define-type Shape-List
(U 'empty-shape-list Shape-List-Cons))
(define-struct Shape-List-Cons
([shape : Shape]
[rest : Shape-List]))The Shape-List type is an example of an inductive type,
i.e., a type that is defined by one or more base cases (e.g., 'empty-shape-list)
and one or more inductive cases (e.g., Shape-List).
Inductive types are naturally processed by recursive functions. When writing recursive functions over inductive types, we usually follow a standard pattern of base cases for the base cases in the type definition and recursive cases for the inductive cases in the type definition. For example, say we want to write a recursive function to count the number of shapes in a list. We start with the header and a skeleton:
(: count-shapes : Shape-List -> Natural)
;; count the number of shapes in a list
;;
(define (count-shapes cl)
(match cl ...)We then add a clause to the match for our base case: the empty list, which has length 0:
(define (count-shapes cl)
(match cl
['empty-shape-list 0]
...)We also need a recursive case for the non-empty list. In that situation, the length of the list will be one plus the length of the rest of the list. The complete function is
(define (count-shapes cl)
(match cl
['empty-shape-list 0]
[(Shape-List-Cons _ r) (+ 1 (count-shapes r))]))Polymorphic functions and types
Just as functions allow us to abstract over specific values, polymorphism allows us to abstract over types.
Consider the following definition of pairs of integers with a function for swapping values:
(define-struct Two-Ints ([fst : Integer] [snd : Integer]))
(: swap-ints : Two-Ints -> Two-Ints)
(define (swap-ints pair)
(match pair [(Two-Ints a b) (Two-Ints b a)]))And this similar definition of pairs of booleans:
(define-struct Two-Bools ([fst : Boolean] [snd : Boolean]))
(: swap-bools : Two-Bools -> Two-Bools)
(define (swap-bools pair)
(match pair [(Two-Bools a b) (Two-Bools b a)]))These types and functions have the same structure, but we had to write them twice in order to get the types right.
When we have a family of function and/or type definitions that are parametric in their definition, we can use polymorphic definitions that allow us to write one implementation that can be used at many types. The idea is very similar to writing functions as a way to parameterize dynamic behavior, but in this case we are parameterizing static behavior.
For example, we can define a polymorphic representation of pairs
(define-struct (Two-Things A B) ([fst : A] [snd : B]))
(: swap : (All (A B) (Two-Things A B)-> (Two-Things B A)))
(define (swap pair)
(match pair [(Two-Things a b) (Two-Things b a)]))In the define-struct, we have introduced two type variables A and B,
which represent the types of the first and second elements (resp.). This
declaration defines a type constructor Two-Things. Type constructors are
functions that make a type out of other types (we have already seen two built-in
type constructors: U and ->). We can now represent pairs of integers
as the type (Two-Things Integer Integer) and pairs of Booleans as (Two-Things Boolean Boolean).
|
Note
|
The syntax of |
We also use type variables in the definition of the polymorphic swap function.
The syntax
(All (A B) (Two-Things A B) -> (Two-Things B A))is called universal quantification and it means "for all types A and B a function
from (Two-Things A B) to (Two-Things B A)". If we apply swap to a value
of type (Two-Things Integer Boolean)
(swap (Two-Things 42 #t))we will get back a value of type (Two-Things Boolean Integer).
(Two-Things #t 42)Type instantiation
Sometimes it is necessary to instantiate a polymorphic function at a specific
type. We use the inst special form to do this operation. The syntax is
(inst id ty1 ty2 ...)where id is the polymorphic function and the ty1, ty2, … are type arguments
(one per variable in id's type). For example, we can instantiate the type of swap
by giving it two type arguments:
(: swap-ib : (Two-Things Integer Boolean) -> (Two-Things Boolean Integer))
(define swap-ib
(inst swap Integer Boolean))If, when working with polymorphic functions, you receive a type checker error
that does not seem to indicate any actual mismatch in types, you may need to
use inst to provide more information about the actual types being used with the function.