[Haskell-cafe] Re: Maybe and partial functions
nicolas.frisby at gmail.com
Tue Mar 13 14:18:01 EDT 2007
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:
> 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.
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe