[Haskell-cafe] Re: Maybe and partial functions

[Nicolas Frisby]

It seems like we could refine the first parameter of carryPropagate
just as the second: make an= type N1 that only admits values [1..].
Would not that suffice to prove that base is never 0 and not have to
go beyond the type-checker for a proof?

On 3/13/07, Neil Mitchell <ndmitchell at gmail.com> wrote:
> 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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>