[Haskell-cafe] Re: Maybe and partial functions

[Neil Mitchell]

Hi Nicolas,

> It seems like we could refine the first parameter of carryPropagate
> just as the second: make an= type N1 that only admits values [1..].

How?

newtype N1 = N1 Int
(put that in a module and don't export N1)

define the constant 2, define the increment operator, change div and mod.

Now we've mainly got a proof in the type checker, but we still don't
actually have a proof for our core N1 definition - but I think that is
probably ok, provided it is a common core which can be reused and is
minimal.

> Would not that suffice to prove that base is never 0 and not have to
> go beyond the type-checker for a proof?

We've now encoded some properties in the type checker, changed most of
the code, and still don't actually have a complete proof. Maybe the
type checker isn't a proof tool ;)

Thanks

Neil