Lists, Generics, and Type Classes

Use the same algorithm with several types.

6.1 A list has two shapes

The standard List(A) consists of the empty list Nil or Cons(head, tail), which stores a first element and the remaining list.

let numbers := Cons(1, Cons(2, Cons(3, Nil)))

fn list_sum(xs: List(i64)): i64 ! {Div} {
  match xs {
    Nil => 0
    Cons(first, rest) => first + list_sum(rest)
  }
}

perform show("sum", list_sum(numbers))

// Recurse over the list structure to add its elements.

・ list_sum

sum = 6

sum = 6

Decomposing a List(i64) by its shape naturally covers both empty and nonempty lists. Recursing on the rest of Cons follows the structure of the list.

6.2 Type-independent functions

fn identity<A>(x: A): A {
  x
}

let n := identity(42)
let t := identity("Tauto")
perform show("n", n)
perform show("t", t)

// The same identity function preserves integers and text.

✓ def identity : ∀ A: Type. (A) -> A

n = 42
t = "Tauto"

n = 42
t = "Tauto"

<A> declares a type parameter. The argument's type determines A, so you can omit it at a call. When applying a type, use parentheses, as in the previous chapter's Option(i64).

6.3 What where Ord(A) means

Comparing values of an arbitrary type requires a comparison operation. Tauto's Ord(A) type class includes not just a comparison function but also the laws an ordering must satisfy. A function declares its requirement with where.

Let's write insertion sort. Import std::Base for proof definitions, and explicitly import std::prelude::Ord for the ordering used by the program.

tauto init sorter

import std::Base
import std::prelude::Ord

pub fn insert<A>(x: A, l: List(A)): List(A) where Ord(A) {
  match l: List(A) {
    Nil => Cons(x, Nil)
    Cons(y, tail) => match Ord::compare(x, y): List(A) {
      Less => Cons(x, Cons(y, tail))
      Equal => Cons(x, Cons(y, tail))
      Greater => Cons(y, insert(x, tail))
    }
  }
}

pub fn sort<A>(l: List(A)): List(A) where Ord(A) {
  match l: List(A) {
    Nil => Nil
    Cons(x, rest) => insert(x, sort(rest))
  }
}

// Insert into an ordered list, then sort the tail recursively.

✓ def insert : ∀ A: Type. (Ord(A)) -> (A) -> (List(A)) -> List(A)
✓ def sort : ∀ A: Type. (Ord(A)) -> (List(A)) -> List(A)

import "sort.taut"

perform show("ints", sort(Cons(3, Cons(1, Cons(2, Nil)))))
perform show("words", sort(Cons("pear", Cons("apple", Cons("fig", Nil)))))

// Reuse one ordering-based algorithm with numbers and words.

ints = Cons(1, Cons(2, Cons(3, Nil)))
words = Cons("apple", Cons("fig", Cons("pear", Nil)))

tauto run --tote sorter

ints = Cons(1, Cons(2, Cons(3, Nil)))
words = Cons("apple", Cons("fig", Cons("pear", Nil)))

If the comparison is Less or Equal, insert at the front; for Greater, inspect the next element. The same sort works with numbers and strings. Ord::compare(x, y) is the comparison operation, and match handles Less, Equal, and Greater.

Because the class is defined so that its laws can be proved, you can state sorting properties independently of a particular numeric type (Chapter 18).

Exercise 6.1: Explain what identity has in common with a function that decomposes a list one layer at a time.