Wolfram Kahl writes:
>
>
> One might even imagine extended instance declarations
> like the following:
>
> > instance Monad []
> > {-# PROOF
> > "Monad-rightId"
> > forall f. f >>= return
> > = concat (map return f)
> > = concat (map (:[]) f)
> > = case f of
> > [] -> concat []
> > (x:xs) -> concat ([x]:map (:[]) xs)
> > = case f of
> > [] -> []
> > (x:xs) -> x : concat (map (:[]) xs)
> > = f
> > "Monad-leftId" ...
> > ...
> > #-}
>
> In the end, my dreams even include a proof format
> that can be checked by the compiler :-)
>
>
>
> Best regards,
>
> Wolfram
>
I enthusiastically support the ability to add properties to the class
declarations. Instead of putting proof texts in the program, I advocate
exporting the class declarations and the properties to a theorem prover.
The class declarations become definitions, and the properties become
proof obligations in the theorem prover. The export from Haskell could
be to some standard intermediate language, which is theorem prover
"agnostic". This intermediate language could be translated to ones
favorite theorem prover, be it HOL, PVS, COQ, ... It is likely that
different theorem provers would be useful for different properties.
Instead of the compiler checking the proofs, a configuration management
system could demand the proofs in some executable (checkable) format.
It is nice to be able to play with the program for a while without
proving it, to get the more mundane errors out before a proof is attempted.
I have found it to be a useless exercise to try and prove code that has
never been executed before.
Having this proof capability would greatly increase the value of Haskell
to my applications here at Motorola.
Cheers
Peter White, Motorola.
