[Haskell-cafe] Re: Maybe and partial functions
ndmitchell at gmail.com
Tue Mar 13 14:28:47 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..].
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
> 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 ;)
More information about the Haskell-Cafe