Edsger Dijkstra said the following of abstraction:
“The purpose of abstraction is not to be vague, but to create a new semantic level in which one can be absolutely precise.”
Abstraction is a cornerstone of programming a complex software system. Without it, a complex software system is a complicated software system. In this article I will explore an important tool in achieving abstraction in programming: function totality.
Motivation
When we write programs, we split them up into smaller components. We do this because most programs are rather complex and it is too hard for us to write a program at once as one monolithic item. Each such smaller component corresponds to a different task that needs to be done by a program. These components can be seen as smaller programs themselves. Once we’re done with smaller components, we compose them into bigger and bigger components that are more complex until we get to our target program. The program works as expected if each of its components works as expected. That is why we have to ensure that each component works as expected in isolation. That way once we are done with a component at an upper level, we don’t have to go back to changing how components at lower levels work to get the component at the upper lower working as needed. This principle is used in so many other domains, for example in assembling a car: you take smaller parts and components and expect them to meet their specifications when putting lots of them together to form a functional car. This is abstraction: not having to worry about or even mention details from lower levels that are irrelevant at a given level.
Exhaustive Pattern-matching
In programming, our abstraction components are functions. Let us say we have the following Haskell function that gets the head element of a list:
head :: [a] -> a
head (x:_) = xIs there something wrong with how the function is defined? There is. It is missing a pattern for an empty input list. This is non-exhaustive pattern matching. The full definition of the function, as given in the base package, is like this:
head :: [a] -> a
head (x:_) = x
head [] = error "Prelude.head: empty list"This definition does pattern-match exhaustively on all forms the input list can take. However, it actually just defers the problem. In particular, in the case of an empty list it calls the error function, which will throw an exception in a problematic way, i.e., without the function declaring in its signature any exceptions to be thrown. The problem cannot be solved by keeping the signature as it is. One way to address the problem is by defining the head function like this:
head :: [a] -> Maybe a
head (x:_) = Just x
head [] = NothingNow it covers all cases and it doesn’t blow up in the user’s face when encountered with a well-typed input.
While it might be easy to spot a missing pattern in this particular example, non-exhaustiveness in general is not as obvious, especially not to GHC, a Haskell compiler that we rely on daily. If you’re to check if a person is at least 18 years old and give them a greeting based on their age and the kind of vehicle they’re driving if they’re at least 18, you would do something like this:
module Greet where
data Vehicle = Car | Motorcycle
data Person = MkPerson Int Vehicle
limit :: Int
limit = 18
greet :: Person -> String
greet (MkPerson age _) | age < limit =
"Be patient, you're not old enough to drive!"
greet (MkPerson age Car) | age >= limit =
"Hello, you car driver!"
greet (MkPerson age Motorcycle) | age >= limit =
"Hello, you motorcycle driver!"While you did cover all possible patterns with such a definition, GHC is not so sure. It reports the following:
$ ghc -Wincomplete-patterns Greet.hs
[1 of 1] Compiling Greet ( Greet.hs, Greet.o )
Greet.hs:11:1: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In an equation for ‘greet’:
Patterns not matched:
(MkPerson _ Car)
(MkPerson _ Motorcycle)
|
11 | greet (MkPerson age _) | age < limit =
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...This happens with GHC 8.6.2, the most recent version as of November 2, 2018. While we are sure that we covered all cases, GHC can’t see that in the case of a person being underage the kind of vehicle the person has does not matter. However, this impedes us from safely using the function in other functions, i.e., at higher levels of abstraction. GHC is warning us we missed some cases and that the function might throw an exception if called with values that meet supposedly not matched patterns.
The challenge for GHC in the example above is in the implicit dependency between the age and the vehicle of a person. Meaningfulness of the vehicle parameter depends on the value of the age parameter: if the age is below 18, the vehicle parameter is irrelevant, and it is relevant only if the age is 18 or more. I found no way to encode this dependency in types in Haskell, though I believe there is a way with one of those libraries attempting to bring dependent types to Haskell (presumably not nice looking). On the other hand, the dependency can be captured in dependently typed programming languages such as Agda and Idris. The following Idris implementation of the greeting example relies on an indexed family of types Person and dependent pattern matching:
module Greet
data Vehicle = Car | Motorcycle
limit : Nat
limit = 18
agePredicate : Nat -> Bool
agePredicate n = n < limit
possiblyVehicle : {p : Nat -> Bool} -> Nat -> Type
possiblyVehicle {p} n = if p n then () else Vehicle
data Person : (a : Nat) -> Bool -> Type where
MkPerson
: (age : Nat)
-> (v : possiblyVehicle {p = agePredicate} age)
-> Person age (agePredicate age)
greet : {age : Nat} -> Person age (agePredicate age) -> String
greet (MkPerson age v) with (agePredicate age)
greet (MkPerson _ ()) | True =
"Be patient, you're not old enough to drive!"
greet (MkPerson _ Car) | False =
"Hello, you car driver!"
greet (MkPerson _ Motorcycle) | False =
"Hello, you motorcycle driver!"If you run :total greet in the Idris REPL, Idris will correctly report that the greet function is total, which implies that we have an exhaustive pattern match, i.e., that we covered all possible well-typed inputs.
Note that in the definition of the MkPerson data constructor in the Idris version we made the type of the v parameter a function of the value of the age parameter. This captures the constraint that an underage person should not operate a vehicle. We can’t do this in the Haskell version of the Person type. Haskellers typically shrug their shoulders and attempt to communicate the inability to capture constraints by specific names of data constructors, e.g., UnsafeMkPerson, which should indicate that a value constructed via this data constructor might not make sense in the problem domain. A slightly better attempt to addressing this issue is via smart constructors, though smart constructors complicate the usage of corresponding types.
Termination
In Haskell and functional programming in general, we like to say that we apply equational reasoning to our code to understand and analyse the code. Let’s see how it works on an example. David Turner has this example in his 2004 paper Total Functional Programming:
loop :: Int -> Int
loop n = 1 + loop nAs you might have noticed, this is an infinite loop, i.e., a program that never terminates. Turner looks at the case when n is 0:
loop 0 = 1 + loop 0and subtracts loop 0 from both sides assuming x - x = 0 to get:
0 = 1We get falsity from an infinite loop under the Curry-Howard isomorphism. This is equivalent to being able to construct a value of an empty type (also called the bottom type) that has no values, i.e. no data constructors.
Turner points out that the value of loop 0 is not an integer of the familiar kind, but rather an integer type extended with a bottom. The value in question is an undefined integer. Falsity arises with unrestricted recursion and therefore this function is partial, unlike usual functions in mathematics.
If we ignored either a non-exhaustive or a non-terminating function and proceeded to functions at a higher level of abstraction that use this problematic function, we would be in trouble: these higher-level functions either wouldn’t be terminating or would throw an exception to the user due to a non-exhaustive pattern match. In either case, the ability to move without a worry to higher levels of abstraction is impeded due to partial functions at lower levels.
Determining if a program terminates, i.e., finishes running for a given input is a decision problem. In particular, it is the halting problem. Thanks to Alan Turing, we know the halting problem is undecidable over Turing machines. In other words, in general we can’t write a program that will tell for an arbitrary program and input whether it terminates. However, Idris, Agda and similar programming languages (proof assistants) can say for many functions that these functions definitely terminate. The idea is, therefore, to program with functions that these languages can confirm to be terminating.
One can also write their own termination proofs in a dependently typed language. First, a data type denoting relation termination is introduced and then using, say, proof of termination via a measure function, one can prove their program to be terminating. For more on writing termination proofs, I recommend a book Verified Functional Programming in Agda by Aaron Stump, and in particular its chapter 9 on formalising deductive systems.
Productivity
So far we considered programs that consume data and that we expect to terminate. What about programs that produce data?
There are programs that are never supposed to terminate, for example operating systems and web servers. Is there even any difference between an infinite loop of the loop function and an ever-running program that produces data? One might jump to a conclusion that we’re on our own with ever-running programs and that we can’t get help from a compiler.
What matters in programs that run forever is that they don’t get stuck. They have to guarantee to be making progress. They have to be productive. In other words, such a program for some well-typed input has to produce some output and continue running. For example, a web server has to provide a response to an HTTP request and go back to listening for new incoming requests.
Essentially, to guarantee that a function is productive, we have to make sure it does not get into a non-productive infinite loop. One way to do that is to provide the so called fuel to a function: on every run when it produces a result it also consumes a drop of fuel and makes a recursive call with the reduced fuel, which guarantees it will consume fuel eventually, getting to a base case of no fuel. Because e.g. a web server actually has to run forever, we provide it with an infinite amount of fuel. This is an adopted excerpt from a book Type-driven development with Idris:
module RunFuel
%default total
data Fuel = Dry | More (Lazy Fuel)
partial
forever : Fuel
forever = More forever
data InfIO : Type where
Do : IO a -> (a -> Inf InfIO) -> InfIO
infProg : InfIO
infProg = Do (putStrLn "Lambda") (\_ => infProg)
run : Fuel -> InfIO -> IO ()
run (More fuel) (Do c f) = do res <- c
run fuel (f res)
run Dry _ = putStrLn "Out of fuel"
partial
main : IO ()
main = run forever infProgThe run function consumes one drop of fuel in its every run and passes the leftover fuel to a recursive call to itself.
We call the run function with an infinite amount of fuel that will keep it running forever. In that way, we pushed non-termination of our program to the edges as much as possible, thereby opening the possibility to make run a terminating function.
Totality
Having seen termination and productiveness, there is a concept that encompasses both termination and productiveness of functions. It is called totality. I’ll take a definition of function totality from the Idris book:
“A total function is a function that, for all well-typed inputs, does one of the following: a) terminates with a well-typed result, or b) produces a non-empty finite prefix of a well-typed infinite result in finite time.”
It is interesting to note that Idris and Agda determine if a function is total purely based on the function’s syntax; the languages do not attempt to understand the semantics of the function. This is how Edwin Brady explains this in his book on Idris:
“Idris considers a function to be total if there are patterns that cover all well-typed inputs, and it can determine that one of the following conditions holds: 1) when there’s a recursive call (or a sequence of mutually recursive calls), there’s a decreasing argument that converges toward a base case, 2) when there’s a recursive call as an argument to Delay, the delayed call will always be an argument to a data constructor (or sequence of nested data constructors) after evaluation, for all inputs.”
Here, Delay is a function that wraps a value with Inf, a type constructor of potentially infinite computations.
If one writes the infinite loop example in Idris, they will see that the example does not pass the totality checker and an error is reported at compile-time. Therefore, Idris and its totality checker are a useful tool to programmer: for a function that is supposed to terminate, the totality checker will check if it will give a result in finite time, and for a function that is supposed to run forever, it will check that it is productive, i.e., that the function is always producing data.
A program often has a terminating and a non-terminating component. The terminating component should be proved total. The non-terminating component can’t always be guaranteed total as a whole. If nothing else, a program always has at least one partial function, which is the main function. Nevertheless, we should strive to have as few partial functions in our programs as possible, because in the case of a program crash we know for sure we have to check only partial functions. This makes it easier to debug and to find the root cause.
Partiality dominates totality in the sense that if a function is partial, all functions calling it will be partial too. The converse is not true: if a function is total, other functions calling it are not automatically guaranteed to be total. That is why it is an imperative in (functional) programming to write total functions.
Another thing to note about total functions is that when it comes to their behavior, it does not matter whether such functions are implemented in a strict evaluation or a non-strict language.
The error function
I’ve been interested in Haskell’s error function from the perspective of totality. There is an equivalent function in Idris too. In essence, the function throws an exception when called. No surprise in Haskell: no totality checking and I guess there is no at least a check for an indirect call to error. However, I am baffled by Idris reporting the following toNat function to be total. The error function throws an exception (which is not declared in the toNat function’s type), yet pure functional languages (Haskell and Idris supposedly are such languages) don’t throw exceptions, and totality is an even stronger property than purity:
module TotalError
import Debug.Error
%language ElabReflection
total
toNat : Maybe Nat -> Nat
toNat Nothing = error "No number here!"
toNat (Just n) = nI am still hoping someone will clarify the totality of the error function in Idris to me. It seems that Agda does not have an error function.
Conclusion
If you are interested to learn more on the topic of function totality in programming, there are several resources I recommend:
- David Turner’s paper Total Functional Programming,
- While their book definitely covers dependently typed theory, I barely started reading it, but totality is at least defined in a new book by Friedman and Christiansen, The Little Typer, in chapter 3. It is possible that totality is considered in later parts of the book, but I’m still reading it,
- As mentioned earlier, Aaron Stump’s book Verified Functional Programming in Agda and its chapter 9 cover termination proofs,
- Edwin Brady’s book Type-driven Development with Idris covers totality extensively. The book drives home the point of types and totality going hand in hand and forming a key abstraction tool.
In conclusion, function totality is important in programming because it helps us build levels of abstractions. We make functions at lower levels of abstractions total, which gives us assurance that they work for all well-typed inputs. Furthermore, for terminating functions we know they will eventually give a result. For possibly infinite computations, we have a guarantee they will be productive and will not e.g. result in a deadlock in a communicating system. Thanks to totality, we can use equational reasoning. In Haskell we only assume to be writing total functions. Haskell’s GHC compiler provides no support in totality checking, so when programming in Haskell, a programmer has to be careful when applying equational reasoning and do totality checking by hand, which obviously leaves a lot of room for making mistakes. Unlike Haskell’s compiler, Idris’ and Agda’s compilers help a programmer with totality checking, thanks to which the programmer can safely apply equational reasoning.