Termination checking in functional programs

Question

Are there functional languages that can specify, in the typechecker, whether or not a certain computation is guaranteed to terminate? Alternatively, can you do this in just Haskell?

Regarding Haskell, in this answer the poster says that

The usual way of thinking about this is that every Haskell type is "lifted"--it contains ⊥. That is, Bool corresponds to {⊥, True, False} rather than just {True, False}. This represents the fact that Haskell programs are not guaranteed to terminate and can have exceptions.

On the other hand, this paper about Agda states that

A correct Agda program is one which passes both type-checking and termination-checking

I.e., all Agda programs will terminate, and a Bool in Agda corresponds to exactly {True, False}.

So for example, in Haskell you can have a value of type IO a, which tells the typechecker that IO is needed to compute the value in question. Could you have a type Lifted a which asserts that the computation in question may not terminate? That is, you allow non-termination, but separate it in the type system. (Obviously, as in Agda, you can only separate values into "definitely terminates" and "might not terminate") If not, are there languages that do this?

Answer 1

You certainly could. However it wouldn't be perfect. By definition, some computations which are terminate would have to reside in Lifted. This is called the halting problem.

Now before you give up on this idea, this isn't as bad is at sounds. Coq, Agda, and many others all work just fine with heuristics for checking termination.

The languages where this actually matters are in ones like Coq and Agda where you're trying to prove theorems. For example, let's say we have the type

 Definition falsy := exists n, n > 0 /\ 0 > n.
 -- Read this as, 
 --   "The type of a proof that for some number n, n > 0 and n < 0"

In Coq syntax. /\ means and. Now to prove such a property in Coq or Agda, we'd have to write something like

Definition out_proof : falsy = ____.
-- Read this as
--   "A proof that there exists a number n < 0 and n > 0"

Where ____ is a proof that for some number n, n > 0 and 0 > n. Now this is awfully hard, since well, falsy is false. Clearly no number exists that is both less than and greater than 0.

However, if we allowed nontermination with unbounded recursion,

 Definition bottom_proof : falsy = bottom_proof.

This type checks, but is obviously inconsistent! We just proved something false! Thus theorem proving assistants enforce some form of termination checking, otherwise they're worthless.

If you wanted to be pragmatic, you could use this lifted type to basically tell the typechecker, "Back off, I know this may not terminate but I'm ok with it". Which is helpful for writing real world stuff like say, a webserver or whatever where you might want it to run "forever".

In essence you're proposing a divide in the language, on one hand, you have "verified code" that you can safely prove things about, and on the other you have "unsafe code" which could loop forever. You're right with the comparison to IO. This is exactly the same idea as Haskell's partitioning of side effects.

Edit: Corecursive data

You mentioned corecursive data, but this isn't quite what you want. The idea is that you do loop forever, but you do so "productively". In essence with recursion the simplest method of checking you terminate is that you always recurse with a term strictly smaller than what you currently have.

Fixpoint factorial n := match n with
  | 0 => 1
  | S n' => n * factorial n'

With corecursion your resulting term must be "bigger" than your input.

Cofixpoint stream := Cons 1 stream

Again this doesn't allow for

 Cofixpoint stream := stream