[Haskell-cafe] Re: Maybe and partial functions

[Neil Mitchell]

Hi

Note: Total = total ignoring non-termination, for this post

> Surely we can assume them total given that base is never zero?

They are not total, they are called in a manner which does not cause
them to raise an error. If you want every function to be total, you
need to fix div.

If you are happy with individual functions being partial, provided the
program as a whole is total, that's fine (and I'd agree with you!).
However, in this case you need to either prove that the program won't
crash, or stop calling it total. This corresponds to proving that base
is never zero.

Of course, if you're going to just accept a proof that base is never
zero, why not just accept a proof that head/tail are called on an
infinite list? It says you defining codata, and your own versions of
head/tail/drop etc

I have a machine checkable (and machine generated) proof that base is
never zero, and the list is infinite.

Thanks

Neil