Posts tagged Dependent Types

Quicksort in Coq

:: Coq, Dependent Types

Coq’s support for dependent types mean that type checking not only catches trivial errors like passing an integer to a function expecting a string, but it can also check and verify types which represent properties regarding the functional behavior of the a program.

I thought it would be edifying to use this capability to write a verified version of quicksort (i.e. a quicksort with types that specify its behavior), and it was!

Total List Functions

:: Coq, Dependent Types

What is the type of a function which returns the first element of a list? One possible (and likely common) answer would be:

1
(: first (All (X) ((Listof X) -> X)))

This (typed racket syntax) says first is a function from a list of X’s to an X (where X is any type). However, we really know that, although its type is ((Listof X) -> X), if we pass an empty list of X we will not get an X, but a runtime error of some sort (e.g. no values). The type then isn’t really giving us a guarantee of what it will do for us… it’s just telling us what it will try to do for us if it doesn’t fail.

“No. Try not. Do… or do not. There is no try.” - Master Yoda

There is a parallel in math: some functions are not defined for all possible input values (e.g. f(x)=1/x). These are called partial functions (as opposed to total functions). It is common practice to reserve the term “function” for total functions in math, while in programming partial functions are ubiquitous and there is little effort to distinguish between the two. If only there was some way that the types could reflect this possibility…