Lambda the Ultimate

My idea was to allow recursion only through a modified y-combinator y :: (a -> a) -> M a where M is the 'recursion' monad. Any use of this y would automatically result in values tainted by the monad. I think that by Curry-Howard it corresponds to a modal logic where you're allowed to use circular arguments in a way that means that you're still protected from being able to prove _|_.

Tarmo Uustalu (with Thorsten Altenkirch and Venanzio Capretta) have done some work on capturing non-termination in the monad

codata Sometime a = Now a | Later (Sometime a)

This talk is about an approach to partiality from non-termination as a monadic effect using coinductive types. The intuitive idea is very simple: termination/non-termination is about waiting, this waiting can be made official. Looping is supported directly by the monad. In order to obtain general recursion, we use that the homsets of the Kleisli category are domains. This gives us a possibility to translate a language with general recursion into a total language following the general paradigm of monadic translation. We also discuss a combination of partiality with other effects based on a monad transformer.

codata Sometime a = Now a | Later (Sometime a)

This idea was often discussed on comp.lang.functional a couple years ago (and probably several times since then).

...included partiality as an example of a monadic side-effect.

From a proof-theoretic point of view, I think that nontermination is best treated as a side-effect. However, from a semantic point of view it has a very special status: the possibility of nontermination is at the heart of domain theory, and is basically why you can give a nontrivial semantics to the untyped lambda calculus (ie, solve a domain equation of the form D == D -> D).

'cuz then their limit is still succ(...(zero)...).

Well, currently Haskell has its I/O requirements in types. And if you are working in a terminating language, it seems like you should almost already know the time complexity of your algorithms (Maybe requiring people to do a complexity analysis instead of a termination proof would be an easier sell?). So now we just need to get space usage factored into the equation. I wonder if a language like Hume has anything to offer in this regard.

And if you are working in a terminating language, it seems like you should almost already know the time complexity of your algorithms (Maybe requiring people to do a complexity analysis instead of a termination proof would be an easier sell?)

I doubt that. Can you give an example of an algorithm which time complexity is easier to analyse than its termination behaviour?

Key word that I guess I should have emphasized: almost. The idea here is that by putting a little more effort into your termination proof, you might also be able to prove the complexity of your algorithm, and subsequently reap those additional rewards. (Certainly termination is a precondition on complexity. If you know the complexity of something, you also already know it terminates).

Do you know of any way to automatically compute reasonably tight complexity of code? Termination is most generalized version of a complexity bound, and there are plenty of languages that only include
terminating programs. Getting more specific there are programming languages characterizing complexity classes, like polynomial time, and logarithmic space. sized types keep track of some sorts of constant factors, but I don't recall that paper bounded the resource requirements of functions, just that they would eventually terminate.

Yes, but immediately after this they point out: [sic]

Runciman [Runciman 1989] gives a useful and interesting discussion of how to
make natural arithmetic closed. He argues rather presuasively that the basic
arithmetic type in a functional language should be Nat rather than Int. In a
total language it is certainly desirable to have Nat as a staticly recognised type,
even if Int is also provided, since there are functions that have no sensible value
on negative integers – factorial for example.

..and I tend to agree: I'd rather have this handled by types (or explicit tests) than exceptions. But this has discussed here before..

Since they are trying to remove "undefined" results, including errors, I don't think its too much to ask.

His natural number arithmetic makes a−b equal to 0 if a<b. Making operations total by giving them artificial results outside their natural (no pun intended) domain is counter-productive. It leads to less robust programs, the converse of the stated goal.

max(0,a-b) is called 'combinatorial subtraction.' I vaguely remember an interesting paper on the subject by Steve Johnson (author of the original Portable C Compiler) from around 1974, but I'll be damned if I can find the reference.

Colin Runciman: What About the Natural Numbers.

...here.

But seriously...if you want total programming then it seems clear to me that

(/) :: Int -> Int -> 1+Int

where you can call the single element of 1 whatever you like: e.g. Exception, DivisionByZero, Infinity, Sigfpe, and you need a convenient way (eg. a monad) to lift computations on Int to computations on 1+Int. I can't see that anything more than this is needed. Certainly no need to make 0/0=0 or ditch the negative numbers.

What should the caller of the / function do with the potential singularity in the result, if he is quite sure that the divisor will never be zero? The contract of the caller probably leaves no space for reporting the problem. It's a total language after all, the caller must return a valid answer to its caller, it can't even loop forever!

One non-solution is to extend the interface of every potentially failing function with a singularity, even if the failure is never intended to happen, and propagate it. This leaks implementation details to interfaces (a sorting function might have a superfluous singularity in its result just because it uses division somewhere), and many practical non-leaf functions are total only in theory. Propagating singularities calls for language support, and if a large function returns a singular result it might be a challenge to find out which of its components has triggered it and why.

Another non-solution is to put bogus values of correct types in these impossible branches. This is a horrible consequence of having to program in a total language.

I don't believe in total programming at all. Pretending that functions don't fail has no value if the way the functions are actually written contains various impossible failures in their code paths. Ruling failures out statically is impractical with present type systems.

Current languages generally offer one of two choices:

1. A computation may abort the whole program, possibly with a message (Haskell's error function). This can happen at any time.
2. Any computation may throw an exception, which can be caught.

The second choice is a superset of the first choice, and thus it's almost universal. Even Glasgow Haskell reinterprets Haskell 98's non-catchable failures as catchable exceptions. I've heard of no paradigm which would offer something better here.

The contract of the caller probably leaves no space for reporting the problem.

This kind of 'reporting' can be conveniently wrapped up in a monad or idiom, or some such device. It doesn't have to be that much of a burden.

Propagating singularities calls for language support,

Or some higher order functions to plumb everything together.

if a large function returns a singular result it might be a challenge to find out which of its components has triggered it and why.

On the contrary. Though I doubt that total functional programming is practical (we agree on that, I just consider this to be an academic exercise), if there's one thing going for it, it's that it won't be as much of a challenge to find why a singular result was created because developers will be encouraged to explicitly handle singular cases. (My nickname came about as a result of spending so much time trying to track down mysterious SIGFPEs because in partial languages developers are not encouraged to implement code to handle singular values.)

What should the caller of the / function do with the potential singularity in the result, if he is quite sure that the divisor will never be zero?

A solution I'm working on basically requires a proof that the divisor will never be zero. If the programmer is quite sure a proof should be wrote down an passed to the compiler. Using qualified types to denote propositions and proofs of its propositions as evidence (as in type classes' instance dictionaries):

(/) :: (Nonzero i) => int -> i -> int
foo a b c = if a == 0 then bar c else baz b / a

In the example a proof is created by the compiler that in the else branch "a" isn't zero. If no proof is provided the proposition would be propagated to foo's caller. If we allow intersection/union types we could extend division's type with | (Zero z, Nonzero i) => z -> i -> z and get a nice optional optimization.
The idea isn't infeasible, though it would probably make compilation times longer if the compiler is expected to infer properties. OTOH if the programmer is supposed to provide the proofs the compiler just needs to check them, which is quite practical. A way to make this process simpler is to provide a sophisticated language for writing proofs and an interactive tool to help nail them down, both would be similar to current theorem provers, and the written proofs would work like proof-carrying code.

Note that, mathematically, division by zero often occurs by rewriting an equation, where said rewriting is actually invalid when division by zero occurs...
Or, in other words, there is often a perfectly sensible result corresponding to this case.

Off the top of my head, I think of

• averages: if there are zero terms to average, the average is undefined.
• roots of second-order polynomials - e.g. a x^2 + b x + c = 0.
  Using the standard formula (-b +/- sqrt(b^2 - 4ac))/2a is invalid when a==0, but a==0 means the actual equation is
  b x + c = 0,
  and so the solution actually is x = -c/b, NOT "undefined".

• someone mentioned factorial.
  If we work with the gamma function, n! = gamma(n+1),
  and 0! = gamma(1) = 1.
  - but whether this is applicable depends on the origin of the factorial term.

So, generally, a "singularity" should be treated with care mathematically, not just in terms of "division errors".

But seriously...if you want total programming then it seems clear to me that
(/) :: Int -> Int -> 1+Int

I don't understand why 0/0 = 0 is any more wrong than 5/3 = 1.

If you want total programming with totally meaningful results, don't you need something like

data Rational = Rational Int Int
(/) :: Int -> Int -> Rational


where the denominator is allowed to be zero?

(1) There are several kinds of division with different applications. Sometimes you want -5/3=-1, sometimes you want -5/3=minus five thirds, sometimes you want -1.66667 and sometimes you want -2. I've met applications where all of these are useful (and most popular programming languages I know offer more than one of these operations). But in my experience, almost every time I've had code attempt to divide by zero the cause has been a bug in the code. I think that's the primary reason to handle division by zero differently.

(2) Division is just an example. I think we're really talking about mathematical exceptions in general. What should the return type of sqrt or acos be? We need to deal with these properly in total functional programming.

What's one-third of five dollars? (possible answer $2, $1, $1.66, $1.67). (Now if I can just install a program to transfer those fractional cents to my bank account).

The most common place I encountered division by zero was in embedded systems, where a value will theoretically approach zero, but due to inaccuracies in measurement may result in a division by zero that has to be caught.

I've been wondering why (high-level) programming languages don't have a slew of different classes like this to represent the type of where your calculation is going. To my mind (and I'm not an academic, so I've ignorance a'plenty) this is a much more serious concern than whether or not the program halts.

It took me quite a while to realise that Coq was a really good system for total functional programming. I think it isn't generally advertised as such, and the tutorials available don't really give the impression that it is a good functional programming environment.

I hope that more examples and tutorials on doing software verification and total functional programming in Coq end up on the web. I'd write one myself but I'm not yet competent enough.

Adam Chlipala has done a lot of work using Coq as a programming language.

My thesis research centers on building programming language tools with proofs of total correctness, using the Coq proof assistant. What distinguishes my approach is that I use dependent types in the implementations of the tools, not just their correctness proofs, following a kind of "correctness by construction" discipline.

See specifically his paper Thoughts on Programming with Proof Assistants - "My purpose in this position paper is to make the general claim that Coq is already quite useful today for non-trivial certified programming tasks..."