Hi, 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?
For example: > multiply :: Num a => a -> a -> a > multiply_group :: Proof Bool > multiply_group = group multiply 1 > group :: (a -> a -> a) -> a -> Proof Bool > group f ident = [proof| f, [associative, identity 1]] 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). Then we might even be able to list properties with class declarations. The properties get verified at compile time. > class Monoid a where > mzero :: a > msum :: a -> a -> a > property a [associative msum, identity mzero msum] Any thoughts? Vivian
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
