1.4 Partial Functions and Nontermination
In Hackett, functions are generally expected to be total, which means they should produce a result for all possible inputs. For example, not is obviously defined for both True and False, which are the only possible values of the Bool type. Total functions allow a programmer to reason about programs using the types alone; a function with the type {A -> B} implies that is is always possible to get a B when you have an A.
Controlling Evaluation in The Hackett Reference has additional information on partial functions.
Sometimes, however, this is impractical. Sometimes the type system is not expressive enough to constrain the input type as much as the programmer would like. In other cases, the burden of assigning a precise type to a value might be too high. In these situations, Hackett allows the programmer to define partial functions. Partial functions should be used extremely judiciously—when a partial function is evaluated at runtime, the program will crash, producing an error message.
Hackett provides a built-in partial function named error! for signaling unrecoverable errors. This function is not only partial, it is actually undefined for all possible values! This partiality can be observed in error!’s type:
> (#:type error!) : (forall (a) {String -> a})
The error! function seems impossible, since it promises to produce anything, of any type, when given nothing but a string. Indeed, this type signature lies; it promises it will produce anything, but this is only possible because it will never actually return anything. When error!’s result is needed, the program will simply crash.
> (: (error! "urk!") Unit) urk!
Partial functions in Hackett are idiomatically indicated by including a ! symbol at the end of their names, but this is only a convention; it is not enforced by the compiler or typechecker.
The error! function can be considered a way to subvert the type system. Its primary purpose is to provide a programmer the ability to mark cases which are “impossible” based on the logic of the program, but the typechecker cannot determine that is true. Of course, in practice, things that where once truly impossible may eventually become possible as code changes, so using some other notion of failure (such as returning a value wrapped in Maybe) is generally preferred whenever possible.
In addition to error!, another partial value provided by Hackett is undefined!. This is a value, not a function, and it miraculously has any type. The undefined! value will crash the program as soon as it is evaluated, but it is often useful for getting something to typecheck before you have finished implementing all of the cases. Generally, undefined! can be useful as a tool while iteratively writing code, but all uses of undefined! should be replaced by “real” implementations before the code is considered complete.
Interestingly, while error! and undefined! crash the program, it is not impossible to write a functions with the same type signatures, but which do not crash the program. How? Well, it’s true that a function that promises to return a value of any type the caller asks for can never return, but there is another possibility besides halting: the function can simply infinitely loop. Here is an example of such a function, called diverge!:
(defn diverge! : (forall [a] {String -> a}) [[x] (diverge! x)])
This sort of function is often also considered partial, since it does not return a value for all of its inputs.
It’s important to keep in mind that Hackett is lazy, and use of partial functions does not change that! This can result in curious behavior, where a partial function does not cause a program to halt or diverge, simply because it isn’t evaluated:
> (const Unit (error! "never gets here"))
: Unit
Unit
In fact, a partial function can “lurk” in an unevaluated thunk for quite a long time, but forcing its evaluation will cause its effects to become visible. These unpredictable effects are another reason to use partial functions extremely sparingly.
Partial values that, once evaluated, will trigger partial behavior are known as bottoms. Documentation of certain forms and functions may note that something is true “ignoring bottom”. This is because many guarantees can technically be broken when partial functions are involved, but it is often more useful to temporarily pretend they do not exist in order to reason about some code using types alone. This is a powerful property of Hackett’s type system; do not squander that power with reckless use of partiality.