Expressive Types

Martin Sulzmann

Overview

Software has bugs
Build software that is correct by construction
Make use of expressive types to achieve this goal

By expressive types we mean:

Exploit the programming language’s type system to catch bugs at compile-time instead of run-time

Next, we take a look at a series of Go examples. The complete program code can be found here.

Example: Physical units

Here is a standard school book exericse:

Given some rectangle where the length and height are record by variables l and h.
Compute the rectangle’s perimeter based on the formula 2 * (l + h).

Below is an implementation in Go.

func perimeterRec(l int, h int) int {
    return l + l + h + h
}

func ex_rec() {
    length := 10 // measured in feet

    height := 5 // measured in meters

    p := perimeterRec(length, height)

    fmt.Printf("\np = %d", p)
}

Any issues?

Length is measured in feet
Height is measured in meters
The physical units do not match

Hence, we might get some bogus result but the program runs just fine and the bug (physical unit mismatch) goes undetected.

Expressive types to the rescue

Idea:

Each variable that stores a distance carries additional information about its physical unit
Arithmetic operation ensure that physical units are consistent with each other

Here’s how we achieve this in Go.

Physical units aware integer variables

type dist[A any] struct {
    val int
}

func add[A any](x dist[A], y dist[A]) dist[A] {
    return dist[A]{x.val + y.val}
}

The actual distance is stored in an integer variable (val)
The type parameter A represents some physical unit
When building a concrete distance value, type parameter A will be instantiated
The type of the add function ensures that the physical units of the to be added value match

Here’s a recast of the above example where we assume the physical units feet and meters.

type meters struct{}
type feet struct{}


func perimeterRec_safe(l dist[meters], h dist[meters]) dist[meters] {
    return add(l, add(l, add(h, h)))
}

func ex_rec_safe() {
    length := dist[meters]{10}

    height := dist[meters]{5}

    p := perimeterRec_safe(length, height)

    fmt.Printf("\np = %d", p.val)
}

/*

func ex_rec_wont_compile() {
    length := dist[feet]{10}

        height := dist[meters]{5}

        p := perimeterRec_safe(length, height)

        fmt.Printf("\np = %d", p.val)
    }

*/

Extensions

As you have noticed, instead of 2 * (l + h) we use the (equivalent) expression l+l+h+h.

If we include multiplication, matters become more complicated.

We need to represent phyisical units such as meters / feet
We need to take care of algebraic unit laws such as (meters * meters) / feet equals meters

It’s possible to represent some more complex phyiscal units in Go but things become more complicated.

Example: Extracting the head element of a slice

Consider the following program text.

func head(xs []int) int {
    return xs[0]
}

func ex_hd() {
    xs := []int{1, 2, 3}
    // The following variant yields panic.
    /// xs := []int{}
    x := head(xs)

    fmt.Printf("\n%d", x)

}

Here’s a variant where we catch the bug (extracting the head of an empty slice) at run-time.

func head_rt(xs []int) (int, bool) {
    if len(xs) == 0 {
        return 0, false
    }

    return xs[0], true
}

func ex_hd_rt() {
    xs := []int{1, 2, 3}

    x, b := head_rt(xs)
    if !b {
        fmt.Println("some panic, do something")
    }
    fmt.Printf("\n%d", x)

}

Challenge:

We wish to catch “head applied on empty slice” at compile-time

Expressive types to the rescue

Idea:

Encode natural numbers at the level of types
Each slice maintains some type information that correspends to its length.

Encoding numbers at the level of types

type zero struct{}

type succ[T nat] struct {
    succ T
}

type nat interface {
    length() int
}

func (x zero) length() int {
    return 0
}

func (x succ[T]) length() int {
    return 1 + x.succ.length()
}

Length-indexed lists

type list[T any, L nat] struct {
    list []T
}

func head_list[T any, L nat](xs list[T, succ[L]]) T {
    return xs.list[0]
}

func push_back[T any, L nat](xs list[T, L], x T) list[T, succ[L]] {
    var ls []T
    ls = append(xs.list, x)
    return list[T, succ[L]]{ls}
}

func mk_list1[T any](x T) list[T, succ[zero]] {
    xs := []T{x}
    return list[T, succ[zero]]{xs}
}

func mk_list0[T any]() list[T, zero] {
    xs := []T{}
    return list[T, zero]{xs}
}

Here’s a recast of the above example where we make use of length-indexed lists.

func ex_hd_list() {
    xs := mk_list0[int]()
    ys := push_back(xs, 1)
    x := head_list(ys)

    fmt.Printf("\n%d", x)
}

Summary and some references

Expressive types are an old idea (they also appear under many names, e.g., phantom types, …)

It’s possible to encode expressive types in today’s programming languages (Go, Java, …)

The future:

We no longer write programs
Instead we specify properties via types and use proof assistants to establish that the properties hold

Some references

Robert Harper, Type systems for programming languages

Benjamin Pierce’s book collection: