One thing you may have noticed in our discussion of binary trees is that we only talked about binary trees that hold Integers. Of course, it's not hard to imagine what a StringTree or RealTree might look like:
(define-type StringTree (U 'Empty StringNode))
(define-struct StringNode
([value : String]
[left-sub : StringTree]
[right-sub : StringTree]))
(define-type RealTree (U 'Empty RealNode))
(define-struct RealNode
([value : Real]
[left-sub : RealTree]
[right-sub : RealTree]))
So that wasn't so bad! In fact, it was quite simple. However, this produces another issue: all of the convenient tree operations we've written are written for IntTrees. So we'd need to change the definition of, say, tree-size like so:
(: tree-size (-> StringTree Integer))
;; Counts the number of nodes in the given binary tree
(define (tree-size t)
(match t
['Empty 0]
[(StringNode _ left right) (+ 1 (tree-size left) (tree-size right))]))
At first glance, this looks almost exactly the same as our previous tree-size function. On closer inspection, yeah, it basically is the same, but with IntTree replaced with StringTree. Of course, this is basically the same as what we did when we changed the definition of IntTree in the first place.
This is the promise of polymorphism. Let's see this in action.
(define-type (Tree A) (U 'Empty (Node A)))
(define-struct (Node A)
([value : A]
[left-sub : (Tree A)]
[right-sub : (Tree A)]))
Here, we need some new terminology to discuss what's happening. Before, we just had types, which were named and defined. However, now that we have polymorphism, we can create new types on the fly, according to a template. We call these type constructors.
We happen to have seen other type constructors before. For instance, U is a type constructor for union types, while -> can be thought of as a type constructor for function types. As we've seen, these are not types themselves, but they are used to define different kinds of types.
In our current case, Tree A and Node A are type constructors, both of which happen to contain a type variable, A. Here, the type variable acts much like an ordinary variable, in that it is a placeholder for something (the something in this case being a type). If you attempt to use them as written, without replacing the variable with an actual type, Racket will not recognize them as types.
Suppose we want to define a Tree that holds Integer. We can do the following:
(: t (Tree Integer))
(define t (Node 31
(Node 15 'Empty 'Empty)
(Node 27
'Empty
(Node 42 'Empty 'Empty))))
Now, suppose we want to define a Tree that holds Strings. Then our definition looks like the following:
(: t (Tree String))
(define t (Node "cat"
(Node "dog"
'Empty
(Node "horse" 'Empty 'Empty))
'Empty))
This seems straightforward to work with, and we attempt the following.
(: tree-size (-> (Tree A) Integer))
;; Counts the number of nodes in the given binary tree
(define (tree-size t)
(match t
['Empty 0]
[(Node _ left right) (+ 1 (tree-size left) (tree-size right))]))
If you tried running the above, you will notice that it does not work. Why? Here, Racket believes that A is the name of a type. For instance, if we have
(: tree-size (-> (Tree Integer) Integer))
;; Counts the number of nodes in the given binary tree
(define (tree-size t)
(match t
['Empty 0]
[((Tree Integer) _ left right) (+ 1 (tree-size left) (tree-size right))]))
there is no reason for Racket to assume that Integer is a type variable. We need some additional information. Here's how to do it:
(: tree-size (All (A) (-> (Tree A) Integer)))
;; Counts the number of nodes in the given binary tree
(define (tree-size t)
(match t
['Empty 0]
[((Tree A) _ left right) (+ 1 (tree-size left) (tree-size right))]))
Here, we have yet another type constructor, All. Here, All (A) can be read "for all $A$", or more specifically, "for all types $A$". This is read in the same way as a universal quantifier: $\forall x$ is read "for all $x$". In effect, All tells the type checker that the following names (in this case, A) are actually type variables to be quantified over the rest of the type.
So we can read the type
(All (A) (-> (Tree A) Integer))
as "for all types A, a function that takes a Tree A as input and produces an Integer".
Here's another example. Recall our structure, the Point:
(define-struct Point
([x : Real]
[y : Real]))
This is a fine type for representing a point on the Euclidean plane. However, you might notice that it's not too different from pairs of arbitrary types. For example, if we wanted to define a pair of an Integer and a String, we'd define something like
(define-struct IntStringPair
([int : Integer]
[str : String]))
And we can begin to see the issue: it's the same thing, just with different types! We can apply our knowledge of polymorphism again and define a structure for arbitrary pairs.
(define-struct (Pairof A B)
([fst : A]
[snd : B]))
Here, fst stands for "first" and snd stands for "second".
Notice that we're not restricted to dealing with only a single type variable. This allows us to do some interesting things, like have pairs of arbitrary type. For example, we could consider a type like
(Pairof Image (Pairof Integer Integer))
to be a pair of an image and its dimensions. Of course, one might protest and say that (Pairof Integer Integer) doesn't tell us much about the intended information, except that it's a pair of Integers. But recall that we have a mechanism for giving names to types! We can do this to enrich our typing:
(define-type Dim (Pairof Integer Integer)) ; Dim for "dimensions"
(Pairof Image Dim)
In the same way, we can define Point by
(define-type Point (Pairof Real Real))
This means that we aren't in any danger of losing anything in terms of expressivity and descriptiveness with types, but we save a lot of work in coming up with definitions.