Posts tagged 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!
What is the type of a function which returns the first element of a list? One possible (and likely common) answer would be:
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…