
On Sat, 24 Jun 2006, Paul Hudak
Hmmm... never tried to write all this down in one place before, but I think this covers all cases:
A partial list is one that ends in _|_. A total list is one that ends in []. A finite list is either partial or total. Any other list is infinite.
To confuse the picture more I'd like to point out that some use different terminology: * A strictly (spine-) partial list is one that ends in _|_. * A (spine-) total list is one that ends in [] or doesn't end at all. * A finite list is one that ends (with [] or _|_). * An infinite list is one that doesn't end. The two concepts (finite/infinite and total/strictly partial) are orthogonal, and both partition the set of all lists. And of course this generalises to other data types: Finite: x is finite if it is contained in all ω-chains whose lubs are x. Infinite: Not finite. Total: No bottoms. Strictly partial: Not total. Partial: Total or strictly partial. -- /NAD