An advantage of explicit partiality

Suppose you have two computations which potentially diverge, and want to run both, returning a result if either of the computations return with a result. How can you accomplish this?

With naïve implementations of these computations in most programming languages, the task is impossible (barring perhaps use of concurrency primitives whose complexity is overkill here). This is because the partiality of these two computations is implicit in their code; that is, they are partial due to the use of fundamental programming constructs such as general recursion or while loops.

Often those who encounter languages marketed as “total” such as Coq and Agda doubt that these languages can be pragmatic. They fear that they will be unable to write computations which potentially diverge. It is true that Coq and Agda forbid implicit partiality; they keep you honest! If you claim to produce a value of type A, you must guarantee you produce such a value.

But it is easy to introduce explicit partiality with a higher-order coinductive type we’ll call Partial (using Coq notation here):

CoInductive Partial (A : Type) :=
  | Now   :         A -> Partial A
  | Later : Partial A -> Partial A.

The Now constructor provides a value of type A, while the Later constructor provides a suspended (total) computation that, when run, produces a Partial A. Now we can loop:

CoFixpoint loop {A : Type} : Partial A := Later loop.

Partial forms a monad:

Definition unit {A : Type} (x : A) : Partial A := Now x.

CoFixpoint join {A : Type} (ppx : Partial (Partial A)) : Partial A :=
  match ppx with
  | Now px => px
  | Later ppx' => Later (join ppx')
  end.

Let’s return to the original question: how do we merge two partial computations to return a result if either of them eventually returns a result? With explicit partiality, it’s a straightforward functional program:

CoFixpoint parallel_or {A : Type} (px py : Partial A) : Partial A
  := match px with
  | Now x => Now x
  | Later px' => match py with
    | Now y => Now y
    | Later py' => parallel_or px' py'
    end
  end.

One can introduce explicit partiality in many programming languages, but few, such as Coq, facilitate guaranteeing the lack of implicit partiality. By forbidding implicit partiality, Coq achieves the best of both worlds. Because Coq is total, its type system funtions as a logic. Totality also yields other benefits: for instance, strict and lazy evaluation always return the same answer, and parametricity theorems are stronger. By allowing explicit partiality with the coinductive Partial type, Coq is easily seen as Turing-complete. Even if we wish to write functions which are in fact provably total in Coq’s logic, we can avoid having to bake the termination proof into the function definition itself (which in general can cause an arbitrarily large blow-up factor in code size; see Bob Harper’s Old neglected theorems are still theorems). Best of all, we can compute the parallel-or for any partial computations.