Hi,<br><br>I have no understanding of template haskell and thus this
message is uninformed speculation. Would it not be possible to write a
function verifier in TH that, unlike QuickCheck which provides bounds
on a function being probably approximately correct, is given a list
over properties which are proven over a quasi-quoted syntax tree?<br>
<br>For example:<br><br>> multiply :: Num a => a -> a -> a<br><br>> multiply_group :: Proof Bool<br>> multiply_group = group multiply 1<br><br>> group :: (a -> a -> a) -> a -> Proof Bool<br>
> group f ident = [proof| f, [associative, identity 1]]<br><br>where
`associative` and `ident` are proof-constructing functions that act
over the `f` syntax tree. (Maybe some invokation of an Isabelle-like
theorem prover or an SMT-like solver as part of the 'proof' module).<br>
<br>Then we might even be able to list properties with class declarations. The properties get verified at compile time.<br><br>> class Monoid a where<br>> mzero :: a<br>> msum :: a -> a -> a<br><br>> property a [associative msum, identity mzero msum]<br>
<br>Any thoughts?<br><br>Vivian<br>
<br>