In Haskell, the list monad provides a way to do non-deterministic, backtracking computations. For example, you can generate all sums of two numbers between 1 and 5 like so:
sums = do x <- [1..5] -- let x be a number between 1 and 5 y <- [1..5] -- let y be a number between 1 and 5 return (x+y) -- return their sum
It will proceed like so: let x be 1; let y be 1; output 1+1; let y be 2; output 1+2; let y be 3; output 1+3; ...; let x be 2; let y be 1; output 2+1; .... If you don't see how cool that is, that's okay, but trust me that it's damn cool. Especially so when you combine this with conditions (i.e. I could have generated all such prime sums), arbitrary recursion.
However, when you enter the realm of the infinite, this is not quite ideal. For example, let's say you're generating ordered pairs like so:
sums = do x <- [1..] -- let x be a number >= 1 y <- [1..] -- let y be a number >= 1 return (x,y) -- return the ordered pair
The enumeration proceeds as before: let x be 1; let y be 1; return (1,1); let y be 2; return (1,2); let y be 3; return (1,3); .... If you're observant, then you'll notice that x will never get to be 2, or any higher number. The entire (reachable) list of ordered pairs has first element 1. If you're going to be searching through the generated possibilities for the pair (3,4), your algorithm will go into an infinite loop. (Maybe you are starting to see the parallel to my last post). Technically, the order type of the returned list is greater than ω, so some elements will take an infinite amount of time to reach.
So what we would like is a list monad where the returned results always come in a list of order type ω, that is, every element can be reached in an (arbitrarily large) finite amount of time. I've written one. The fundamental idea is that of the standard well-ordering of the rationals. Consider this grid:
1,1 1,2 1,3 1,4 1,5 ... 2,1 2,2 2,3 2,4 2,5 ... 3,1 3,2 3,3 3,4 3,5 ... ...
You can put this into a list of order type ω by traversing the positive diagonals: 1,1; 2,1; 1,2; 3,1; 2,2; 1,3; 4,1; 3,2; 2,3; 1,4; ...
So basically, whenever the algorithm joins two lists, it does it not by concatenating them together (as the standard list monad does), but by "diagonalizing" them together. This ensures that if you only feed it lists of order type omega, it will output a list of order type omega.
Incidentally, this provides a kernel for the logic engine I was talking about. This will enumerate all logical sentences in order type omega, so that if you look through the list for sentences that are true, you will eventually get to a true statement if there is one.