Totality can be split into two separate properties:
- All programs are defined for all inputs (exhaustive)
- All programs terminate/coterminate
The former is becoming more common (like your Rust example), but the latter isn't very widespread. For example, most would consider a function like this to be exhaustive, even though it loops forever when both Ints are non-zero:
foo : (Int, Int) -> Int
foo (0, y) = y
foo (x, y) = foo (y, x)
Proving termination is hard, and often undesirable; e.g. we want servers and operating systems to keep running indefinitely. However, co-termination can be quite easy, e.g. if we define a Delay (co)datatype:
data Delay t where
Now : t -> Delay t
Later : Delay t -> Delay t
Wrapping recursive calls in 'Later' allows infinite processes, at the cost of some boilerplate (Delay is a monad, if you know what that is):
foo : (Int, Int) -> Delay Int
foo (0, y) = Now y
foo (x, y) = Later (foo (y, x))
- All programs are defined for all inputs (exhaustive)
- All programs terminate/coterminate
The former is becoming more common (like your Rust example), but the latter isn't very widespread. For example, most would consider a function like this to be exhaustive, even though it loops forever when both Ints are non-zero:
Proving termination is hard, and often undesirable; e.g. we want servers and operating systems to keep running indefinitely. However, co-termination can be quite easy, e.g. if we define a Delay (co)datatype: Wrapping recursive calls in 'Later' allows infinite processes, at the cost of some boilerplate (Delay is a monad, if you know what that is):