Polymorphism

In this chapter, we continue our development of basic programming concepts. Our new essential principles are polymorphism (abstraction functions over the data types they manipulate) and higher-order functions (treating functions as data). We begin with polymorphism.

Polymorphic Lists

In the last two chapters, we worked with polymorphic lists, you may just not have realized it. Obviously, interesting programs also need to be able to manipulate lists with elements of other types - lists of strings, lists of booleans, lists of lists, etc. We could just define a new inductive data type for each of them, for example...

type BoolList {
   nil 
   cons (head: Bool) (tail: List Bool) 
}

...but that would quickly become tedious, in part because we have to compensate for different constructor names for each data type, but mainly because we also need to define new versions of all our list manipulation functions (length, rev, etc.) for each new data type definition.

To avoid all this repetition, Kind supports definitions of polymorphic inductive types. For example, here is a polymorphic list data type that we already saw in the previous chapter:

type List (t) {
   nil 
   cons (head: t) (tail: List t) 
}

This type already exists in Kind and we can see that it is identical to BoolList, but with a type a, which receives any other type, be it Nat, Bool, Maybe, etc. We don't need to create a list type for each of the data types, we can use this one that adopts all existing forms.

What kind of thing is the List itself? A good way to think about it is that List is a Types function for inductive definitions; or, in other words, List is a Types function for Types. For any specific type x, the type List x is an inductively defined set of lists whose elements are of type x.

With this definition, when we use the constructors List.nil and List.cons to build lists, we need to tell Kind the type of elements in the lists we are building - that is, that List.nil and List.cons are now polymorphic constructors. Note the types of constructors:

record Pair (a) (b) {
  fst : a
  snd : b
}

Our Pair type receives two other types, a and b, and returns a pair of the two types. It was not necessary to define whether the pair was of natural numbers, booleans, lists, bits or other pairs, we left the function capable of handling all possible pairs and this is thanks to polymorphism.

Now we can go back and make polymorphic versions of all the processing lists functions we wrote before. Here's the repeat function again, for example:

Repeat <a: Type> (x: a) (count: Nat) : List a
Repeat a x Nat.zero                  = List.nil
Repeat a x (Nat.succ count)          = List.cons x (Repeat x count)

Just like with List.nil and List.cons, we can use repeat by first applying it to a type and then to its list argument:

Test_repeat1 : Equal (Repeat 4n 2n) (List.cons 4n (List.cons 4n List.nil))
Test_repeat1 = Equal.refl

To use repeat to build other types of lists, we simply instantiate it with an appropriate type parameter:

Test_repeat2 : Equal (Repeat Bool.false 1n) (List.cons Bool.false List.nil)
Test_repeat2 = Equal.refl

Type Annotation Inference

Let's write the definition of repeat again, but this time omitting the type. However, please note that this is not a good practice to use the hole, it will only serve to understand the power of Kind and how it can help the user find what they want.

Repeat (x: _) (count: Nat) : List _
Repeat x Nat.zero          = ?

When running the Type Check, the terminal returns:

+ INFO  Inspection.

   • Expected: (List _) 

   • Context: 
   •   x : _ 

   Repeat x Nat.zero = ?
                       ┬
                       └Here!

For the case where the count is zero, which is our stopping point, we need to return a list of undefined type.

As we did when our type was defined, we are creating a list that does not repeat the term at all, we return a List.nil, then we check for the case of a list that will repeat the value count times, for this we will use recursion through Nat.succ pred, that is, our count is equal to the successor of its predecessor.

Repeat x (Nat.succ count) = ?

And the Type Check returns:

+ INFO  Inspection.

   • Expected: (List _) 

   • Context: 
   •   x     : _ 
   •   count : Nat 

   Repeat x (Nat.succ count) = ?
                               ┬
                               └Here!

Now we just need to construct the list with the value and call the function for the predecessor of count, thus building the list until it reaches zero.

Repeat (x: _) (count: Nat) : List _
Repeat x Nat.zero          = List.nil
Repeat x (Nat.succ count)  = List.cons x (Repeat x count)

We can see that, even though we didn't define the type of x, the Kind is powerful enough to discover the type that our x is when we use the _ hole. Although it is possible and may even facilitate building an entire application using this notation, it is not a good practice since, depending on the case, a different type than the desired one may be inferred. It is interesting to always define the type of our element, even if it is a polymorphic type.

In the first case, when we define the type a, we already encompass all possible types, so it is not necessary to use the hole and that is the magic of polymorphism, it allows us to use the same function for different types.

To use a polymorphic function, we need to pass one or more types in addition to the other arguments. For example, in the case of repeat, we pass the type <a: Type> and that each element of our list is of that type. We did the same with the Pair type, which received two types a and b as arguments.

Now it is much easier to understand the examples we used in the previous chapter, when we presented functions like length and append:

Length <a> (xs: List a) : Nat
Length (List.nil t)            = Nat.zero
Length (List.cons t head tail) = (Nat.succ (Length tail))

Concat <a: Type> (xs: List a) (ys: List a) : List a
Concat (List.nil)                     ys = ys
Concat (List.cons head tail)          ys = List.cons head (Concat tail ys)

Note that there are two notations, one where we only use <a> and another where we use <a: Type>, we can use either one, the Kind is capable of understanding both forms, it will be up to the developer to choose which one to use and the complexity of what will be developed, since in very complex code, it may be interesting to make explicit to other programmers what each thing is.

Now it's time to implement our functions with implicit typing, using hole and sugar syntax:

Concat_implicito (xs: List _) (ys: List _) : List _
Concat_implicito []                     ys = ys
Concat_implicito (List.cons head tail)  ys = List.cons head (Concat_implicito tail ys)

Here we learned one more thing, the sugar syntax for an empty list is just [], but this is wrong, since the sugar syntax for kind doesn't work on the left side of the function scope, only on the right side. Using the wrong sugar syntax results in an error shown by Kind:

- ERROR  Unexpected token '['.
    Concat_implicito []  ys = ys
                  ┬
                  └Here!

Therefore, it is always important to know exactly what is being done, especially when using sugar syntax. It is meant to make our lives easier but can cause problems when used incorrectly. This also applies to hole and polymorphic types help us write a safer program that can be used for countless cases.

We can also rewrite the reverse function:

Rev <a> (xs: List a) : List a
Rev List.nil              = [] // sugar syntax de List.nil
Rev (List.cons head tail) = Concat (Rev tail) [head] // sugar syntax de (List.cons head List.nil)

Length <a> (xs: List a) : Nat
Length List.nil              = 0n // sugar syntax de Nat.zero
Length (List.cons head tail) = Nat.succ (Length tail)

After that, we just need to prove that our functions are correct:

Test_rev1 : Equal (Rev [1,2,3]) [3,2,1]
Test_rev1 = Equal.refl

Test_rev2 : Equal (Rev [Bool.true]) [Bool.true]
Test_rev2 = Equal.refl

Test_length1 : Equal (Length [1,2,3]) 3n
Test_length1 = Equal.refl

Polymorphic Exercises

Here are some simple exercises, similar to the ones in the Lists section, to practice polymorphism. Complete the proofs below.

Concat_nil_r <a> (xs: List a) : Equal (Concat xs List.nil) xs
Concat_nil_r xs = ?

Concat_assoc <a> (xs: List a) (ys: List a) (zs: List a) : Equal (Concat xs (Concat ys zs)) (Concat (Concat xs ys) zs)
Concat_assoc xs ys zs = ?

Concat_length <a> (xs: List a) (ys: List a) : Equal (Length (Concat xs ys)) (Plus (Length xs) (Length ys))
Concat_length xs ys = ?

More Polymorphic Exercises

Here are some slightly more interesting exercises...

Rev_app_distr <a> (xs: List a) (ys: List a) : Equal (Rev (Concat xs ys)) (Concat (Rev ys) (Rev xs))
Rev_app_distr xs ys = ?

Rev_involutive <a> (xs: List a) : Equal (Rev (Rev xs)) xs
Rev_involutive xs = ?

Polymorphic Pairs

Following the same pattern, the type definition for pairs of numbers that we gave in the last chapter can be generalized for polymorphic pairs:

record Pair (a) (b) {
  fst : a
  snd : b
} 

This is exactly the first definition of pairs that we saw in the previous chapter, and now we can understand perfectly what the a and b types are in the Pair type definition.

We can rewrite the Pairs functions, but now for polymorphic types:

Fst <a> <b> (pair: Pair a b) : a
Fst (Pair.new fst snd) = fst

Snd <a> <b> (pair: Pair a b) : b
Snd (Pair.new fst snd) = snd

The following function takes two lists and combines them into a list of pairs. In functional languages, this is commonly called Zip.

Zip <a> <b> (xs: List a) (ys: List b) : (List (Pair a b))
Zip [] ys = []
Zip xs [] = []
Zip (List.cons xs.h xs.t) (List.cons ys.h ys.t) = List.cons (Pair.new xs.h xs.t) (Zip xs.t ys.t)

Check

Without running the program, try to answer the following question:

• What will the combination of [1, 2] and [Bool.true, Bool.false, Bool.false, Bool.true] return?

Now run the code and see if you got it right.

Split

The Split function is the inverse of Zip. It takes a list of pairs and returns a pair of lists. In many functional languages, it is called Unzip.

Fill in the definition of the splitting function below. Make sure it passes the unit test provided.

Split <a> <b> (xs: List (Pair a b)) : Pair (List a) (List b)
Split xs = ?

Test_split : Equal (Split [(Pair.new 1 Bool.false), (Pair.new 2 Bool.false)]) (Pair.new ([1, 2]) ([Bool.false, Bool.false]))
Test_split = ?

Polymorphism with Maybe

In the previous chapter, we also saw the Maybe type, but only for natural types. However, as we have seen in this chapter, our data structures can be polymorphic, which means that the Maybe type is also polymorphic, and that is what we will see now.

type Maybe (t) {
  none 
  some (value: t)
}

This way, we can write the function of the nth error to be used with all types of lists:

Nth_error <a> (n: Nat) (xs: List a) : Maybe a
Nth_error a n List.nil              = Maybe.none
Nth_error a n (List.cons head tail) =
  let ind = Nth_error (Pred n) tail
  Bool.if (Eql n 0n) (Maybe.some head) (ind)


Test_nth_error1 : Equal (Nth_error 0n [4n,5n,5n,7n]) (Maybe.some 4n)
Test_nth_error1 = Equal.refl

Test_nth_error2 : Equal (Nth_error 2n [Bool.true]) Maybe.none
Test_nth_error2 = Equal.refl

Test_nth_error3 : Equal (Nth_error 1n [[1n],[2n]]) (Maybe.some [2n])
Test_nth_error3 = Equal.refl

Hd_error

Complete the definition of a polymorphic version of the Hd_error function from the last chapter. Make sure it passes the unit tests below.

Hd_error <a> (xs: Lista a) : Maybe a
Hd_error xs = ?

Test_hd_error1 : Equal (Hd_error [1, 2]) (Maybe.some 1)
Test_hd_error1 = ?

Test_hd_error2 : Equal (Hd_error [[1], [2]]) (Maybe.some [1])
Test_hd_error2 = ?